mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 21:37:48 +03:00
[ refactor ] Factor out a type for primitive types out of Constant
This commit is contained in:
Denis Buzdalov
G. Allais
parent
9d93e74012
commit
05d64483f6
@ -56,6 +56,8 @@
|
||||
* Adds `%deprecate` pragma that can be used to warn when deprecated functions are used.
|
||||
* Package files now support a `langversion` field that can be used to specify what versions of Idris a package supports. As with dependency versions, `>`, `<`, `>=`, and `<=` can all be used.
|
||||
+ For example, `langversion >= 0.5.1`.
|
||||
* Alternatives for primitive types of the `Core.TT.Constant` are moved out to a separate data type `PrimTypes`.
|
||||
Signatures of functions that were working with `Constant` are changed to use `PrimTypes` when appropriate.
|
||||
|
||||
### IDE protocol changes
|
||||
|
||||
|
||||
@ -64,6 +64,23 @@ data NameType : Type where
|
||||
DataCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
TyCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
|
||||
public export
|
||||
data PrimType
|
||||
= IntType
|
||||
| IntegerType
|
||||
| Int8Type
|
||||
| Int16Type
|
||||
| Int32Type
|
||||
| Int64Type
|
||||
| Bits8Type
|
||||
| Bits16Type
|
||||
| Bits32Type
|
||||
| Bits64Type
|
||||
| StringType
|
||||
| CharType
|
||||
| DoubleType
|
||||
| WorldType
|
||||
|
||||
public export
|
||||
data Constant
|
||||
= I Int
|
||||
@ -79,23 +96,9 @@ data Constant
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
| PrT PrimType
|
||||
| WorldVal
|
||||
|
||||
| IntType
|
||||
| IntegerType
|
||||
| Int8Type
|
||||
| Int16Type
|
||||
| Int32Type
|
||||
| Int64Type
|
||||
| Bits8Type
|
||||
| Bits16Type
|
||||
| Bits32Type
|
||||
| Bits64Type
|
||||
| StringType
|
||||
| CharType
|
||||
| DoubleType
|
||||
| WorldType
|
||||
|
||||
public export
|
||||
data UserName
|
||||
= Basic String -- default name constructor e.g. map
|
||||
|
||||
@ -518,8 +518,8 @@ record ConstantPrimitives where
|
||||
||| the implementations from the provided `ConstantPrimitives`.
|
||||
export
|
||||
castInt : ConstantPrimitives
|
||||
-> Constant
|
||||
-> Constant
|
||||
-> PrimType
|
||||
-> PrimType
|
||||
-> String
|
||||
-> Core String
|
||||
castInt p from to x =
|
||||
|
||||
@ -344,11 +344,8 @@ mutual
|
||||
= pure (CDelay fc lr !(toCExp m n arg))
|
||||
toCExpTm m n (TForce fc lr arg)
|
||||
= pure (CForce fc lr !(toCExp m n arg))
|
||||
toCExpTm m n (PrimVal fc c)
|
||||
= let t = constTag c in
|
||||
if t == 0
|
||||
then pure $ CPrimVal fc c
|
||||
else pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing []
|
||||
toCExpTm m n (PrimVal fc $ PrT c) = pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] -- Primitive type constant
|
||||
toCExpTm m n (PrimVal fc c) = pure $ CPrimVal fc c -- Non-type constant
|
||||
toCExpTm m n (Erased fc _) = pure $ CErased fc
|
||||
toCExpTm m n (TType fc _) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing []
|
||||
|
||||
@ -601,22 +598,22 @@ getNArgs defs n args = pure $ User n args
|
||||
|
||||
nfToCFType : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> (inStruct : Bool) -> NF [] -> Core CFType
|
||||
nfToCFType _ _ (NPrimVal _ IntType) = pure CFInt
|
||||
nfToCFType _ _ (NPrimVal _ IntegerType) = pure CFInteger
|
||||
nfToCFType _ _ (NPrimVal _ Bits8Type) = pure CFUnsigned8
|
||||
nfToCFType _ _ (NPrimVal _ Bits16Type) = pure CFUnsigned16
|
||||
nfToCFType _ _ (NPrimVal _ Bits32Type) = pure CFUnsigned32
|
||||
nfToCFType _ _ (NPrimVal _ Bits64Type) = pure CFUnsigned64
|
||||
nfToCFType _ _ (NPrimVal _ Int8Type) = pure CFInt8
|
||||
nfToCFType _ _ (NPrimVal _ Int16Type) = pure CFInt16
|
||||
nfToCFType _ _ (NPrimVal _ Int32Type) = pure CFInt32
|
||||
nfToCFType _ _ (NPrimVal _ Int64Type) = pure CFInt64
|
||||
nfToCFType _ False (NPrimVal _ StringType) = pure CFString
|
||||
nfToCFType fc True (NPrimVal _ StringType)
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT IntType) = pure CFInt
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT IntegerType) = pure CFInteger
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Bits8Type) = pure CFUnsigned8
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Bits16Type) = pure CFUnsigned16
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Bits32Type) = pure CFUnsigned32
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Bits64Type) = pure CFUnsigned64
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Int8Type) = pure CFInt8
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Int16Type) = pure CFInt16
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Int32Type) = pure CFInt32
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT Int64Type) = pure CFInt64
|
||||
nfToCFType _ False (NPrimVal _ $ PrT StringType) = pure CFString
|
||||
nfToCFType fc True (NPrimVal _ $ PrT StringType)
|
||||
= throw (GenericMsg fc "String not allowed in a foreign struct")
|
||||
nfToCFType _ _ (NPrimVal _ DoubleType) = pure CFDouble
|
||||
nfToCFType _ _ (NPrimVal _ CharType) = pure CFChar
|
||||
nfToCFType _ _ (NPrimVal _ WorldType) = pure CFWorld
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT DoubleType) = pure CFDouble
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT CharType) = pure CFChar
|
||||
nfToCFType _ _ (NPrimVal _ $ PrT WorldType) = pure CFWorld
|
||||
nfToCFType _ False (NBind fc _ (Pi _ _ _ ty) sc)
|
||||
= do defs <- get Ctxt
|
||||
sty <- nfToCFType fc False !(evalClosure defs ty)
|
||||
|
||||
@ -307,6 +307,9 @@ boundedUIntOp = boundedOp "u"
|
||||
boolOp : (op : String) -> (lhs : Doc) -> (rhs : Doc) -> Doc
|
||||
boolOp o lhs rhs = "(" <+> binOp o lhs rhs <+> "?1:0)"
|
||||
|
||||
jsPrimType : PrimType -> String
|
||||
jsPrimType _ = "#t"
|
||||
|
||||
-- convert an Idris constant to its JS representation
|
||||
jsConstant : Constant -> String
|
||||
jsConstant (I i) = show i
|
||||
@ -315,28 +318,15 @@ jsConstant (I16 i) = show i
|
||||
jsConstant (I32 i) = show i
|
||||
jsConstant (I64 i) = show i ++ "n"
|
||||
jsConstant (BI i) = show i ++ "n"
|
||||
jsConstant (Str s) = jsString s
|
||||
jsConstant (Ch c) = jsString $ singleton c
|
||||
jsConstant (Db f) = show f
|
||||
jsConstant WorldVal = esName "idrisworld"
|
||||
jsConstant (B8 i) = show i
|
||||
jsConstant (B16 i) = show i
|
||||
jsConstant (B32 i) = show i
|
||||
jsConstant (B64 i) = show i ++ "n"
|
||||
jsConstant IntType = "#t"
|
||||
jsConstant Int8Type = "#t"
|
||||
jsConstant Int16Type = "#t"
|
||||
jsConstant Int32Type = "#t"
|
||||
jsConstant Int64Type = "#t"
|
||||
jsConstant IntegerType = "#t"
|
||||
jsConstant Bits8Type = "#t"
|
||||
jsConstant Bits16Type = "#t"
|
||||
jsConstant Bits32Type = "#t"
|
||||
jsConstant Bits64Type = "#t"
|
||||
jsConstant StringType = "#t"
|
||||
jsConstant CharType = "#t"
|
||||
jsConstant DoubleType = "#t"
|
||||
jsConstant WorldType = "#t"
|
||||
jsConstant (Str s) = jsString s
|
||||
jsConstant (Ch c) = jsString $ singleton c
|
||||
jsConstant (Db f) = show f
|
||||
jsConstant (PrT t) = jsPrimType t
|
||||
jsConstant WorldVal = esName "idrisworld"
|
||||
|
||||
-- Creates the definition of a binary arithmetic operation.
|
||||
-- Rounding / truncation behavior is determined from the
|
||||
@ -353,11 +343,11 @@ arithOp _ "" op = integerOp op
|
||||
arithOp _ sym _ = binOp sym
|
||||
|
||||
-- use 32bit signed integer for `Int`.
|
||||
jsIntKind : Constant -> Maybe IntKind
|
||||
jsIntKind IntType = Just . Signed $ P 32
|
||||
jsIntKind : PrimType -> Maybe IntKind
|
||||
jsIntKind IntType = Just . Signed $ P 32
|
||||
jsIntKind x = intKind x
|
||||
|
||||
jsMod : Constant -> Doc -> Doc -> Doc
|
||||
jsMod : PrimType -> Doc -> Doc -> Doc
|
||||
jsMod ty x y = case jsIntKind ty of
|
||||
(Just $ Signed $ P n) => case useBigInt' n of
|
||||
True => integerOp "mod" x y
|
||||
@ -368,7 +358,7 @@ jsMod ty x y = case jsIntKind ty of
|
||||
|
||||
-- implementation of all kinds of cast from and / or to integral
|
||||
-- values.
|
||||
castInt : Constant -> Constant -> Doc -> Core Doc
|
||||
castInt : PrimType -> PrimType -> Doc -> Core Doc
|
||||
castInt from to x =
|
||||
case ((from, jsIntKind from), (to, jsIntKind to)) of
|
||||
((CharType,_), (_,Just k)) => truncInt (useBigInt k) k $ jsIntOfChar k x
|
||||
|
||||
@ -115,7 +115,7 @@ constFold rho (COp {arity} fc fn xs) =
|
||||
fromNF (NPrimVal fc c) = Just $ CPrimVal fc c
|
||||
fromNF _ = Nothing
|
||||
|
||||
commutative : Constant -> Bool
|
||||
commutative : PrimType -> Bool
|
||||
commutative DoubleType = False
|
||||
commutative _ = True
|
||||
|
||||
|
||||
@ -113,6 +113,22 @@ showInt64Min x = if x == -9223372036854775808
|
||||
then "INT64_MIN"
|
||||
else "INT64_C("++ show x ++")"
|
||||
|
||||
cPrimType : PrimType -> String
|
||||
cPrimType IntType = "Int64"
|
||||
cPrimType Int8Type = "Int8"
|
||||
cPrimType Int16Type = "Int16"
|
||||
cPrimType Int32Type = "Int32"
|
||||
cPrimType Int64Type = "Int64"
|
||||
cPrimType IntegerType = "Integer"
|
||||
cPrimType Bits8Type = "Bits8"
|
||||
cPrimType Bits16Type = "Bits16"
|
||||
cPrimType Bits32Type = "Bits32"
|
||||
cPrimType Bits64Type = "Bits64"
|
||||
cPrimType StringType = "string"
|
||||
cPrimType CharType = "char"
|
||||
cPrimType DoubleType = "double"
|
||||
cPrimType WorldType = "f32"
|
||||
|
||||
cConstant : Constant -> String
|
||||
cConstant (I x) = "(Value*)makeInt64("++ showIntMin x ++")"
|
||||
cConstant (I8 x) = "(Value*)makeInt8(INT8_C("++ show x ++"))"
|
||||
@ -120,28 +136,15 @@ cConstant (I16 x) = "(Value*)makeInt16(INT16_C("++ show x ++"))"
|
||||
cConstant (I32 x) = "(Value*)makeInt32(INT32_C("++ show x ++"))"
|
||||
cConstant (I64 x) = "(Value*)makeInt64("++ showInt64Min x ++")"
|
||||
cConstant (BI x) = "(Value*)makeIntegerLiteral(\""++ show x ++"\")"
|
||||
cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"
|
||||
cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")"
|
||||
cConstant (Str x) = "(Value*)makeString("++ cStringQuoted x ++")"
|
||||
cConstant WorldVal = "(Value*)makeWorld()"
|
||||
cConstant IntType = "Int64"
|
||||
cConstant Int8Type = "Int8"
|
||||
cConstant Int16Type = "Int16"
|
||||
cConstant Int32Type = "Int32"
|
||||
cConstant Int64Type = "Int64"
|
||||
cConstant IntegerType = "Integer"
|
||||
cConstant StringType = "string"
|
||||
cConstant CharType = "char"
|
||||
cConstant DoubleType = "double"
|
||||
cConstant WorldType = "f32"
|
||||
cConstant (B8 x) = "(Value*)makeBits8(UINT8_C("++ show x ++"))"
|
||||
cConstant (B16 x) = "(Value*)makeBits16(UINT16_C("++ show x ++"))"
|
||||
cConstant (B32 x) = "(Value*)makeBits32(UINT32_C("++ show x ++"))"
|
||||
cConstant (B64 x) = "(Value*)makeBits64(UINT64_C("++ show x ++"))"
|
||||
cConstant Bits8Type = "Bits8"
|
||||
cConstant Bits16Type = "Bits16"
|
||||
cConstant Bits32Type = "Bits32"
|
||||
cConstant Bits64Type = "Bits64"
|
||||
cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"
|
||||
cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")"
|
||||
cConstant (Str x) = "(Value*)makeString("++ cStringQuoted x ++")"
|
||||
cConstant (PrT t) = cPrimType t
|
||||
cConstant WorldVal = "(Value*)makeWorld()"
|
||||
|
||||
extractConstant : Constant -> String
|
||||
extractConstant (I x) = show x
|
||||
@ -167,12 +170,12 @@ plainOp op args = op ++ "(" ++ (showSep ", " args) ++ ")"
|
||||
|
||||
||| Generate scheme for a primitive function.
|
||||
cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String
|
||||
cOp (Neg ty) [x] = "negate_" ++ cConstant ty ++ "(" ++ x ++ ")"
|
||||
cOp (Neg ty) [x] = "negate_" ++ cPrimType ty ++ "(" ++ x ++ ")"
|
||||
cOp StrLength [x] = "stringLength(" ++ x ++ ")"
|
||||
cOp StrHead [x] = "head(" ++ x ++ ")"
|
||||
cOp StrTail [x] = "tail(" ++ x ++ ")"
|
||||
cOp StrReverse [x] = "reverse(" ++ x ++ ")"
|
||||
cOp (Cast i o) [x] = "cast_" ++ (cConstant i) ++ "_to_" ++ (cConstant o) ++ "(" ++ x ++ ")"
|
||||
cOp (Cast i o) [x] = "cast_" ++ (cPrimType i) ++ "_to_" ++ (cPrimType o) ++ "(" ++ x ++ ")"
|
||||
cOp DoubleExp [x] = "(Value*)makeDouble(exp(unpackDouble(" ++ x ++ ")))"
|
||||
cOp DoubleLog [x] = "(Value*)makeDouble(log(unpackDouble(" ++ x ++ ")))"
|
||||
cOp DoublePow [x, y] = "(Value*)makeDouble(pow(unpackDouble(" ++ x ++ "), unpackDouble(" ++ y ++ ")))"
|
||||
@ -185,21 +188,21 @@ cOp DoubleATan [x] = "(Value*)makeDouble(atan(unpackDouble(" ++ x ++ ")
|
||||
cOp DoubleSqrt [x] = "(Value*)makeDouble(sqrt(unpackDouble(" ++ x ++ ")))"
|
||||
cOp DoubleFloor [x] = "(Value*)makeDouble(floor(unpackDouble(" ++ x ++ ")))"
|
||||
cOp DoubleCeiling [x] = "(Value*)makeDouble(ceil(unpackDouble(" ++ x ++ ")))"
|
||||
cOp (Add ty) [x, y] = "add_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Sub ty) [x, y] = "sub_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Mul ty) [x, y] = "mul_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Div ty) [x, y] = "div_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Mod ty) [x, y] = "mod_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (ShiftL ty) [x, y] = "shiftl_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (ShiftR ty) [x, y] = "shiftr_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (BAnd ty) [x, y] = "and_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (BOr ty) [x, y] = "or_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (BXOr ty) [x, y] = "xor_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (LT ty) [x, y] = "lt_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (GT ty) [x, y] = "gt_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (EQ ty) [x, y] = "eq_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (LTE ty) [x, y] = "lte_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (GTE ty) [x, y] = "gte_" ++ cConstant ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Add ty) [x, y] = "add_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Sub ty) [x, y] = "sub_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Mul ty) [x, y] = "mul_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Div ty) [x, y] = "div_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (Mod ty) [x, y] = "mod_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (ShiftL ty) [x, y] = "shiftl_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (ShiftR ty) [x, y] = "shiftr_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (BAnd ty) [x, y] = "and_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (BOr ty) [x, y] = "or_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (BXOr ty) [x, y] = "xor_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (LT ty) [x, y] = "lt_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (GT ty) [x, y] = "gt_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (EQ ty) [x, y] = "eq_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (LTE ty) [x, y] = "lte_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp (GTE ty) [x, y] = "gte_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp StrIndex [x, i] = "strIndex(" ++ x ++ ", " ++ i ++ ")"
|
||||
cOp StrCons [x, y] = "strCons(" ++ x ++ ", " ++ y ++ ")"
|
||||
cOp StrAppend [x, y] = "strAppend(" ++ x ++ ", " ++ y ++ ")"
|
||||
|
||||
@ -245,6 +245,9 @@ export
|
||||
mkWorld : String -> String
|
||||
mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes
|
||||
|
||||
schPrimType : PrimType -> String
|
||||
schPrimType _ = "#t"
|
||||
|
||||
schConstant : (String -> String) -> Constant -> String
|
||||
schConstant _ (I x) = show x
|
||||
schConstant _ (I8 x) = show x
|
||||
@ -262,21 +265,8 @@ schConstant _ (Ch x)
|
||||
then "#\\" ++ cast x
|
||||
else "(integer->char " ++ show (the Int (cast x)) ++ ")"
|
||||
schConstant _ (Db x) = show x
|
||||
schConstant _ (PrT t) = schPrimType t
|
||||
schConstant _ WorldVal = "#f"
|
||||
schConstant _ IntType = "#t"
|
||||
schConstant _ Int8Type = "#t"
|
||||
schConstant _ Int16Type = "#t"
|
||||
schConstant _ Int32Type = "#t"
|
||||
schConstant _ Int64Type = "#t"
|
||||
schConstant _ IntegerType = "#t"
|
||||
schConstant _ Bits8Type = "#t"
|
||||
schConstant _ Bits16Type = "#t"
|
||||
schConstant _ Bits32Type = "#t"
|
||||
schConstant _ Bits64Type = "#t"
|
||||
schConstant _ StringType = "#t"
|
||||
schConstant _ CharType = "#t"
|
||||
schConstant _ DoubleType = "#t"
|
||||
schConstant _ WorldType = "#t"
|
||||
|
||||
schCaseDef : Maybe String -> String
|
||||
schCaseDef Nothing = ""
|
||||
|
||||
@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
|
||||
||| version number if you're changing the version more than once in the same day.
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 20220208 * 100 + 0
|
||||
ttcVersion = 20220310 * 100 + 0
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
|
||||
@ -1114,10 +1114,9 @@ mkPat args orig (As fc _ _ ptm)
|
||||
= mkPat [] orig ptm
|
||||
mkPat args orig (TDelay fc r ty p)
|
||||
= pure $ PDelay fc r !(mkPat [] orig ty) !(mkPat [] orig p)
|
||||
mkPat args orig (PrimVal fc c)
|
||||
= pure $ if constTag c == 0
|
||||
then PConst fc c
|
||||
else PTyCon fc (UN (Basic $ show c)) 0 []
|
||||
mkPat args orig (PrimVal fc $ PrT c) -- Primitive type constant
|
||||
= pure $ PTyCon fc (UN (Basic $ show c)) 0 []
|
||||
mkPat args orig (PrimVal fc c) = pure $ PConst fc c -- Non-type constant
|
||||
mkPat args orig (TType fc _) = pure $ PTyCon fc (UN $ Basic "Type") 0 []
|
||||
mkPat args orig tm
|
||||
= do log "compile.casetree" 10 $
|
||||
|
||||
@ -160,7 +160,7 @@ getMissingAlts : {auto c : Ref Ctxt Defs} ->
|
||||
Core (List (CaseAlt vars))
|
||||
-- If it's a primitive other than WorldVal, there's too many to reasonably
|
||||
-- check, so require a catch all
|
||||
getMissingAlts fc defs (NPrimVal _ WorldType) alts
|
||||
getMissingAlts fc defs (NPrimVal _ $ PrT WorldType) alts
|
||||
= if isNil alts
|
||||
then pure [DefaultCase (Unmatched "Coverage check")]
|
||||
else pure []
|
||||
|
||||
@ -100,21 +100,21 @@ mutual
|
||||
= bindty
|
||||
|
||||
chkConstant : FC -> Constant -> Term vars
|
||||
chkConstant fc (I x) = PrimVal fc IntType
|
||||
chkConstant fc (I8 x) = PrimVal fc Int8Type
|
||||
chkConstant fc (I16 x) = PrimVal fc Int16Type
|
||||
chkConstant fc (I32 x) = PrimVal fc Int32Type
|
||||
chkConstant fc (I64 x) = PrimVal fc Int64Type
|
||||
chkConstant fc (BI x) = PrimVal fc IntegerType
|
||||
chkConstant fc (B8 x) = PrimVal fc Bits8Type
|
||||
chkConstant fc (B16 x) = PrimVal fc Bits16Type
|
||||
chkConstant fc (B32 x) = PrimVal fc Bits32Type
|
||||
chkConstant fc (B64 x) = PrimVal fc Bits64Type
|
||||
chkConstant fc (Str x) = PrimVal fc StringType
|
||||
chkConstant fc (Ch x) = PrimVal fc CharType
|
||||
chkConstant fc (Db x) = PrimVal fc DoubleType
|
||||
chkConstant fc WorldVal = PrimVal fc WorldType
|
||||
chkConstant fc _ = TType fc (MN "top" 0)
|
||||
chkConstant fc (I x) = PrimVal fc $ PrT IntType
|
||||
chkConstant fc (I8 x) = PrimVal fc $ PrT Int8Type
|
||||
chkConstant fc (I16 x) = PrimVal fc $ PrT Int16Type
|
||||
chkConstant fc (I32 x) = PrimVal fc $ PrT Int32Type
|
||||
chkConstant fc (I64 x) = PrimVal fc $ PrT Int64Type
|
||||
chkConstant fc (BI x) = PrimVal fc $ PrT IntegerType
|
||||
chkConstant fc (B8 x) = PrimVal fc $ PrT Bits8Type
|
||||
chkConstant fc (B16 x) = PrimVal fc $ PrT Bits16Type
|
||||
chkConstant fc (B32 x) = PrimVal fc $ PrT Bits32Type
|
||||
chkConstant fc (B64 x) = PrimVal fc $ PrT Bits64Type
|
||||
chkConstant fc (Str x) = PrimVal fc $ PrT StringType
|
||||
chkConstant fc (Ch x) = PrimVal fc $ PrT CharType
|
||||
chkConstant fc (Db x) = PrimVal fc $ PrT DoubleType
|
||||
chkConstant fc WorldVal = PrimVal fc $ PrT WorldType
|
||||
chkConstant fc _ = TType fc (MN "top" 0)
|
||||
|
||||
export
|
||||
getType : {vars : _} ->
|
||||
|
||||
@ -269,61 +269,43 @@ Hashable CFType where
|
||||
CFInteger =>
|
||||
h `hashWithSalt` 22
|
||||
|
||||
export
|
||||
Hashable PrimType where
|
||||
hashWithSalt h = \case
|
||||
IntType => h `hashWithSalt` 1
|
||||
Int8Type => h `hashWithSalt` 2
|
||||
Int16Type => h `hashWithSalt` 3
|
||||
Int32Type => h `hashWithSalt` 4
|
||||
Int64Type => h `hashWithSalt` 5
|
||||
IntegerType => h `hashWithSalt` 6
|
||||
Bits8Type => h `hashWithSalt` 7
|
||||
Bits16Type => h `hashWithSalt` 8
|
||||
Bits32Type => h `hashWithSalt` 9
|
||||
Bits64Type => h `hashWithSalt` 10
|
||||
StringType => h `hashWithSalt` 11
|
||||
CharType => h `hashWithSalt` 12
|
||||
DoubleType => h `hashWithSalt` 13
|
||||
WorldType => h `hashWithSalt` 14
|
||||
|
||||
export
|
||||
Hashable Constant where
|
||||
hashWithSalt h = \case
|
||||
I i =>
|
||||
h `hashWithSalt` 0 `hashWithSalt` i
|
||||
BI x =>
|
||||
h `hashWithSalt` 1 `hashWithSalt` x
|
||||
B8 x =>
|
||||
h `hashWithSalt` 2 `hashWithSalt` x
|
||||
B16 x =>
|
||||
h `hashWithSalt` 3 `hashWithSalt` x
|
||||
B32 x =>
|
||||
h `hashWithSalt` 4 `hashWithSalt` x
|
||||
B64 x =>
|
||||
h `hashWithSalt` 5 `hashWithSalt` x
|
||||
Str x =>
|
||||
h `hashWithSalt` 6 `hashWithSalt` x
|
||||
Ch x =>
|
||||
h `hashWithSalt` 7 `hashWithSalt` x
|
||||
Db x =>
|
||||
h `hashWithSalt` 8 `hashWithSalt` x
|
||||
I i => h `hashWithSalt` 0 `hashWithSalt` i
|
||||
I8 x => h `hashWithSalt` 1 `hashWithSalt` x
|
||||
I16 x => h `hashWithSalt` 2 `hashWithSalt` x
|
||||
I32 x => h `hashWithSalt` 3 `hashWithSalt` x
|
||||
I64 x => h `hashWithSalt` 4 `hashWithSalt` x
|
||||
BI x => h `hashWithSalt` 5 `hashWithSalt` x
|
||||
B8 x => h `hashWithSalt` 6 `hashWithSalt` x
|
||||
B16 x => h `hashWithSalt` 7 `hashWithSalt` x
|
||||
B32 x => h `hashWithSalt` 8 `hashWithSalt` x
|
||||
B64 x => h `hashWithSalt` 9 `hashWithSalt` x
|
||||
Str x => h `hashWithSalt` 10 `hashWithSalt` x
|
||||
Ch x => h `hashWithSalt` 11 `hashWithSalt` x
|
||||
Db x => h `hashWithSalt` 12 `hashWithSalt` x
|
||||
PrT x => h `hashWithSalt` 13 `hashWithSalt` x
|
||||
|
||||
WorldVal =>
|
||||
h `hashWithSalt` 9
|
||||
|
||||
IntType =>
|
||||
h `hashWithSalt` 10
|
||||
IntegerType =>
|
||||
h `hashWithSalt` 11
|
||||
Bits8Type =>
|
||||
h `hashWithSalt` 12
|
||||
Bits16Type =>
|
||||
h `hashWithSalt` 13
|
||||
Bits32Type =>
|
||||
h `hashWithSalt` 14
|
||||
Bits64Type =>
|
||||
h `hashWithSalt` 15
|
||||
StringType =>
|
||||
h `hashWithSalt` 16
|
||||
CharType =>
|
||||
h `hashWithSalt` 17
|
||||
DoubleType =>
|
||||
h `hashWithSalt` 18
|
||||
WorldType =>
|
||||
h `hashWithSalt` 19
|
||||
|
||||
I8 x => h `hashWithSalt` 20 `hashWithSalt` x
|
||||
I16 x => h `hashWithSalt` 21 `hashWithSalt` x
|
||||
I32 x => h `hashWithSalt` 22 `hashWithSalt` x
|
||||
I64 x => h `hashWithSalt` 23 `hashWithSalt` x
|
||||
|
||||
Int8Type => h `hashWithSalt` 24
|
||||
Int16Type => h `hashWithSalt` 25
|
||||
Int32Type => h `hashWithSalt` 26
|
||||
Int64Type => h `hashWithSalt` 27
|
||||
WorldVal => h `hashWithSalt` 14
|
||||
|
||||
export
|
||||
Hashable LazyReason where
|
||||
|
||||
@ -13,6 +13,26 @@ thenCmp LT _ = LT
|
||||
thenCmp EQ o = o
|
||||
thenCmp GT _ = GT
|
||||
|
||||
export
|
||||
Ord PrimType where
|
||||
compare = compare `on` tag
|
||||
where
|
||||
tag : PrimType -> Int
|
||||
tag IntType = 1
|
||||
tag Int8Type = 2
|
||||
tag Int16Type = 3
|
||||
tag Int32Type = 4
|
||||
tag Int64Type = 5
|
||||
tag IntegerType = 6
|
||||
tag Bits8Type = 7
|
||||
tag Bits16Type = 8
|
||||
tag Bits32Type = 9
|
||||
tag Bits64Type = 10
|
||||
tag StringType = 11
|
||||
tag CharType = 12
|
||||
tag DoubleType = 13
|
||||
tag WorldType = 14
|
||||
|
||||
export
|
||||
Ord Constant where
|
||||
I x `compare` I y = compare x y
|
||||
@ -28,6 +48,7 @@ Ord Constant where
|
||||
Str x `compare` Str y = compare x y
|
||||
Ch x `compare` Ch y = compare x y
|
||||
Db x `compare` Db y = compare x y
|
||||
PrT x `compare` PrT y = compare x y
|
||||
compare x y = compare (tag x) (tag y)
|
||||
where
|
||||
tag : Constant -> Int
|
||||
@ -44,22 +65,8 @@ Ord Constant where
|
||||
tag (Str _) = 10
|
||||
tag (Ch _) = 11
|
||||
tag (Db _) = 12
|
||||
tag WorldVal = 13
|
||||
tag IntType = 14
|
||||
tag Int8Type = 15
|
||||
tag Int16Type = 16
|
||||
tag Int32Type = 17
|
||||
tag Int64Type = 18
|
||||
tag IntegerType = 19
|
||||
tag Bits8Type = 20
|
||||
tag Bits16Type = 21
|
||||
tag Bits32Type = 22
|
||||
tag Bits64Type = 23
|
||||
tag StringType = 24
|
||||
tag CharType = 25
|
||||
tag DoubleType = 26
|
||||
tag WorldType = 27
|
||||
|
||||
tag (PrT _) = 13
|
||||
tag WorldVal = 14
|
||||
|
||||
primFnEq : PrimFn a1 -> PrimFn a2 -> Maybe (a1 = a2)
|
||||
primFnEq (Add t1) (Add t2) = if t1 == t2 then Just Refl else Nothing
|
||||
|
||||
@ -503,26 +503,29 @@ believeMe [_, _, val@(NPrimVal _ _)] = Just val
|
||||
believeMe [_, _, NType fc u] = Just (NType fc u)
|
||||
believeMe [_, _, val] = Nothing
|
||||
|
||||
constTy : Constant -> Constant -> Constant -> ClosedTerm
|
||||
primTyVal : PrimType -> ClosedTerm
|
||||
primTyVal = PrimVal emptyFC . PrT
|
||||
|
||||
constTy : PrimType -> PrimType -> PrimType -> ClosedTerm
|
||||
constTy a b c
|
||||
= let arr = fnType emptyFC in
|
||||
PrimVal emptyFC a `arr` (PrimVal emptyFC b `arr` PrimVal emptyFC c)
|
||||
primTyVal a `arr` (primTyVal b `arr` primTyVal c)
|
||||
|
||||
constTy3 : Constant -> Constant -> Constant -> Constant -> ClosedTerm
|
||||
constTy3 : PrimType -> PrimType -> PrimType -> PrimType -> ClosedTerm
|
||||
constTy3 a b c d
|
||||
= let arr = fnType emptyFC in
|
||||
PrimVal emptyFC a `arr`
|
||||
(PrimVal emptyFC b `arr`
|
||||
(PrimVal emptyFC c `arr` PrimVal emptyFC d))
|
||||
primTyVal a `arr`
|
||||
(primTyVal b `arr`
|
||||
(primTyVal c `arr` primTyVal d))
|
||||
|
||||
predTy : Constant -> Constant -> ClosedTerm
|
||||
predTy : PrimType -> PrimType -> ClosedTerm
|
||||
predTy a b = let arr = fnType emptyFC in
|
||||
PrimVal emptyFC a `arr` PrimVal emptyFC b
|
||||
primTyVal a `arr` primTyVal b
|
||||
|
||||
arithTy : Constant -> ClosedTerm
|
||||
arithTy : PrimType -> ClosedTerm
|
||||
arithTy t = constTy t t t
|
||||
|
||||
cmpTy : Constant -> ClosedTerm
|
||||
cmpTy : PrimType -> ClosedTerm
|
||||
cmpTy t = constTy t t IntType
|
||||
|
||||
doubleTy : ClosedTerm
|
||||
@ -542,10 +545,10 @@ believeMeTy
|
||||
crashTy : ClosedTerm
|
||||
crashTy
|
||||
= pi "a" erased Explicit (TType emptyFC (MN "top" 0)) $
|
||||
pi "msg" top Explicit (PrimVal emptyFC StringType) $
|
||||
pi "msg" top Explicit (PrimVal emptyFC $ PrT StringType) $
|
||||
Local emptyFC Nothing _ (Later First)
|
||||
|
||||
castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castTo : PrimType -> Vect 1 (NF vars) -> Maybe (NF vars)
|
||||
castTo IntType = castInt
|
||||
castTo Int8Type = castInt8
|
||||
castTo Int16Type = castInt16
|
||||
@ -559,7 +562,7 @@ castTo Bits64Type = castBits64
|
||||
castTo StringType = castString
|
||||
castTo CharType = castChar
|
||||
castTo DoubleType = castDouble
|
||||
castTo _ = const Nothing
|
||||
castTo WorldType = const Nothing
|
||||
|
||||
export
|
||||
getOp : {0 arity : Nat} -> PrimFn arity ->
|
||||
@ -655,7 +658,7 @@ opName (Cast x y) = prim $ "cast_" ++ show x ++ show y
|
||||
opName BelieveMe = prim $ "believe_me"
|
||||
opName Crash = prim $ "crash"
|
||||
|
||||
integralTypes : List Constant
|
||||
integralTypes : List PrimType
|
||||
integralTypes = [ IntType
|
||||
, Int8Type
|
||||
, Int16Type
|
||||
@ -668,10 +671,10 @@ integralTypes = [ IntType
|
||||
, Bits64Type
|
||||
]
|
||||
|
||||
numTypes : List Constant
|
||||
numTypes : List PrimType
|
||||
numTypes = integralTypes ++ [DoubleType]
|
||||
|
||||
primTypes : List Constant
|
||||
primTypes : List PrimType
|
||||
primTypes = numTypes ++ [StringType, CharType]
|
||||
|
||||
export
|
||||
|
||||
@ -472,6 +472,41 @@ Reflect NameType where
|
||||
i' <- reflect fc defs lhs env i
|
||||
appCon fc defs (reflectiontt "TyCon") [t', i']
|
||||
|
||||
export
|
||||
Reify PrimType where
|
||||
reify defs val@(NDCon _ n _ _ args)
|
||||
= case (dropAllNS !(full (gamma defs) n), args) of
|
||||
(UN (Basic "IntType"), [])
|
||||
=> pure IntType
|
||||
(UN (Basic "Int8Type"), [])
|
||||
=> pure Int8Type
|
||||
(UN (Basic "Int16Type"), [])
|
||||
=> pure Int16Type
|
||||
(UN (Basic "Int32Type"), [])
|
||||
=> pure Int32Type
|
||||
(UN (Basic "Int64Type"), [])
|
||||
=> pure Int64Type
|
||||
(UN (Basic "IntegerType"), [])
|
||||
=> pure IntegerType
|
||||
(UN (Basic "Bits8Type"), [])
|
||||
=> pure Bits8Type
|
||||
(UN (Basic "Bits16Type"), [])
|
||||
=> pure Bits16Type
|
||||
(UN (Basic "Bits32Type"), [])
|
||||
=> pure Bits32Type
|
||||
(UN (Basic "Bits64Type"), [])
|
||||
=> pure Bits64Type
|
||||
(UN (Basic "StringType"), [])
|
||||
=> pure StringType
|
||||
(UN (Basic "CharType"), [])
|
||||
=> pure CharType
|
||||
(UN (Basic "DoubleType"), [])
|
||||
=> pure DoubleType
|
||||
(UN (Basic "WorldType"), [])
|
||||
=> pure WorldType
|
||||
_ => cantReify val "PrimType"
|
||||
reify defs val = cantReify val "PrimType"
|
||||
|
||||
export
|
||||
Reify Constant where
|
||||
reify defs val@(NDCon _ n _ _ args)
|
||||
@ -515,39 +550,45 @@ Reify Constant where
|
||||
(UN (Basic "Db"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (Db x')
|
||||
(UN (Basic "PrT"), [(_, x)])
|
||||
=> do x' <- reify defs !(evalClosure defs x)
|
||||
pure (PrT x')
|
||||
(UN (Basic "WorldVal"), [])
|
||||
=> pure WorldVal
|
||||
(UN (Basic "IntType"), [])
|
||||
=> pure IntType
|
||||
(UN (Basic "Int8Type"), [])
|
||||
=> pure Int8Type
|
||||
(UN (Basic "Int16Type"), [])
|
||||
=> pure Int16Type
|
||||
(UN (Basic "Int32Type"), [])
|
||||
=> pure Int32Type
|
||||
(UN (Basic "Int64Type"), [])
|
||||
=> pure Int64Type
|
||||
(UN (Basic "IntegerType"), [])
|
||||
=> pure IntegerType
|
||||
(UN (Basic "Bits8Type"), [])
|
||||
=> pure Bits8Type
|
||||
(UN (Basic "Bits16Type"), [])
|
||||
=> pure Bits16Type
|
||||
(UN (Basic "Bits32Type"), [])
|
||||
=> pure Bits32Type
|
||||
(UN (Basic "Bits64Type"), [])
|
||||
=> pure Bits64Type
|
||||
(UN (Basic "StringType"), [])
|
||||
=> pure StringType
|
||||
(UN (Basic "CharType"), [])
|
||||
=> pure CharType
|
||||
(UN (Basic "DoubleType"), [])
|
||||
=> pure DoubleType
|
||||
(UN (Basic "WorldType"), [])
|
||||
=> pure WorldType
|
||||
_ => cantReify val "Constant"
|
||||
reify defs val = cantReify val "Constant"
|
||||
|
||||
export
|
||||
Reflect PrimType where
|
||||
reflect fc defs lhs env IntType
|
||||
= getCon fc defs (reflectiontt "IntType")
|
||||
reflect fc defs lhs env Int8Type
|
||||
= getCon fc defs (reflectiontt "Int8Type")
|
||||
reflect fc defs lhs env Int16Type
|
||||
= getCon fc defs (reflectiontt "Int16Type")
|
||||
reflect fc defs lhs env Int32Type
|
||||
= getCon fc defs (reflectiontt "Int32Type")
|
||||
reflect fc defs lhs env Int64Type
|
||||
= getCon fc defs (reflectiontt "Int64Type")
|
||||
reflect fc defs lhs env IntegerType
|
||||
= getCon fc defs (reflectiontt "IntegerType")
|
||||
reflect fc defs lhs env Bits8Type
|
||||
= getCon fc defs (reflectiontt "Bits8Type")
|
||||
reflect fc defs lhs env Bits16Type
|
||||
= getCon fc defs (reflectiontt "Bits16Type")
|
||||
reflect fc defs lhs env Bits32Type
|
||||
= getCon fc defs (reflectiontt "Bits32Type")
|
||||
reflect fc defs lhs env Bits64Type
|
||||
= getCon fc defs (reflectiontt "Bits64Type")
|
||||
reflect fc defs lhs env StringType
|
||||
= getCon fc defs (reflectiontt "StringType")
|
||||
reflect fc defs lhs env CharType
|
||||
= getCon fc defs (reflectiontt "CharType")
|
||||
reflect fc defs lhs env DoubleType
|
||||
= getCon fc defs (reflectiontt "DoubleType")
|
||||
reflect fc defs lhs env WorldType
|
||||
= getCon fc defs (reflectiontt "WorldType")
|
||||
|
||||
export
|
||||
Reflect Constant where
|
||||
reflect fc defs lhs env (I x)
|
||||
@ -589,36 +630,11 @@ Reflect Constant where
|
||||
reflect fc defs lhs env (Db x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "Db") [x']
|
||||
reflect fc defs lhs env (PrT x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectiontt "PrT") [x']
|
||||
reflect fc defs lhs env WorldVal
|
||||
= getCon fc defs (reflectiontt "WorldVal")
|
||||
reflect fc defs lhs env IntType
|
||||
= getCon fc defs (reflectiontt "IntType")
|
||||
reflect fc defs lhs env Int8Type
|
||||
= getCon fc defs (reflectiontt "Int8Type")
|
||||
reflect fc defs lhs env Int16Type
|
||||
= getCon fc defs (reflectiontt "Int16Type")
|
||||
reflect fc defs lhs env Int32Type
|
||||
= getCon fc defs (reflectiontt "Int32Type")
|
||||
reflect fc defs lhs env Int64Type
|
||||
= getCon fc defs (reflectiontt "Int64Type")
|
||||
reflect fc defs lhs env IntegerType
|
||||
= getCon fc defs (reflectiontt "IntegerType")
|
||||
reflect fc defs lhs env Bits8Type
|
||||
= getCon fc defs (reflectiontt "Bits8Type")
|
||||
reflect fc defs lhs env Bits16Type
|
||||
= getCon fc defs (reflectiontt "Bits16Type")
|
||||
reflect fc defs lhs env Bits32Type
|
||||
= getCon fc defs (reflectiontt "Bits32Type")
|
||||
reflect fc defs lhs env Bits64Type
|
||||
= getCon fc defs (reflectiontt "Bits64Type")
|
||||
reflect fc defs lhs env StringType
|
||||
= getCon fc defs (reflectiontt "StringType")
|
||||
reflect fc defs lhs env CharType
|
||||
= getCon fc defs (reflectiontt "CharType")
|
||||
reflect fc defs lhs env DoubleType
|
||||
= getCon fc defs (reflectiontt "DoubleType")
|
||||
reflect fc defs lhs env WorldType
|
||||
= getCon fc defs (reflectiontt "WorldType")
|
||||
|
||||
export
|
||||
Reify Visibility where
|
||||
|
||||
@ -156,7 +156,7 @@ applyIntCast (Unsigned m) (Unsigned n) x
|
||||
else Apply (Var "ct-cast-unsigned") [x, toScheme n]
|
||||
|
||||
applyCast : SchemeObj Write ->
|
||||
Constant -> Constant ->
|
||||
PrimType -> PrimType ->
|
||||
SchemeObj Write -> SchemeObj Write
|
||||
applyCast blk CharType to x
|
||||
= canonical blk [x] $
|
||||
|
||||
@ -151,12 +151,12 @@ compileConstant fc (B64 x) = Vector (-109) [IntegerVal (cast x)]
|
||||
compileConstant fc (Str x) = StringVal x
|
||||
compileConstant fc (Ch x) = CharVal x
|
||||
compileConstant fc (Db x) = FloatVal x
|
||||
-- Constant types get compiled as TyCon names, for matching purposes
|
||||
compileConstant fc t
|
||||
= Vector (-1) [IntegerVal (cast (constTag t)),
|
||||
compileConstant fc (PrT t) -- Constant types get compiled as TyCon names, for matching purposes
|
||||
= Vector (-1) [IntegerVal (cast (primTypeTag t)),
|
||||
StringVal (show t),
|
||||
toScheme (UN (Basic (show t))),
|
||||
toScheme fc]
|
||||
compileConstant fc WorldVal = Null
|
||||
|
||||
compileStk : Ref Sym Integer =>
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
|
||||
264
src/Core/TT.idr
264
src/Core/TT.idr
@ -59,23 +59,8 @@ covering
|
||||
showCon d "MkKindedName" $ showArg nm ++ showArg @{Raw} fn ++ showArg @{Raw} rn
|
||||
|
||||
public export
|
||||
data Constant
|
||||
= I Int
|
||||
| I8 Int8
|
||||
| I16 Int16
|
||||
| I32 Int32
|
||||
| I64 Int64
|
||||
| BI Integer
|
||||
| B8 Bits8
|
||||
| B16 Bits16
|
||||
| B32 Bits32
|
||||
| B64 Bits64
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
| WorldVal
|
||||
|
||||
| IntType
|
||||
data PrimType
|
||||
= IntType
|
||||
| Int8Type
|
||||
| Int16Type
|
||||
| Int32Type
|
||||
@ -90,8 +75,26 @@ data Constant
|
||||
| DoubleType
|
||||
| WorldType
|
||||
|
||||
public export
|
||||
data Constant
|
||||
= I Int
|
||||
| I8 Int8
|
||||
| I16 Int16
|
||||
| I32 Int32
|
||||
| I64 Int64
|
||||
| BI Integer
|
||||
| B8 Bits8
|
||||
| B16 Bits16
|
||||
| B32 Bits32
|
||||
| B64 Bits64
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
| PrT PrimType
|
||||
| WorldVal
|
||||
|
||||
export
|
||||
isConstantType : Name -> Maybe Constant
|
||||
isConstantType : Name -> Maybe PrimType
|
||||
isConstantType (UN (Basic n)) = case n of
|
||||
"Int" => Just IntType
|
||||
"Int8" => Just Int8Type
|
||||
@ -112,35 +115,22 @@ isConstantType _ = Nothing
|
||||
|
||||
export
|
||||
isPrimType : Constant -> Bool
|
||||
isPrimType (I x) = False
|
||||
isPrimType (I8 x) = False
|
||||
isPrimType (I16 x) = False
|
||||
isPrimType (I32 x) = False
|
||||
isPrimType (I64 x) = False
|
||||
isPrimType (BI x) = False
|
||||
isPrimType (B8 x) = False
|
||||
isPrimType (B16 x) = False
|
||||
isPrimType (B32 x) = False
|
||||
isPrimType (B64 x) = False
|
||||
isPrimType (Str x) = False
|
||||
isPrimType (Ch x) = False
|
||||
isPrimType (Db x) = False
|
||||
isPrimType WorldVal = False
|
||||
isPrimType (PrT _) = True
|
||||
isPrimType _ = False
|
||||
|
||||
isPrimType Int8Type = True
|
||||
isPrimType Int16Type = True
|
||||
isPrimType Int32Type = True
|
||||
isPrimType Int64Type = True
|
||||
isPrimType IntType = True
|
||||
isPrimType IntegerType = True
|
||||
isPrimType Bits8Type = True
|
||||
isPrimType Bits16Type = True
|
||||
isPrimType Bits32Type = True
|
||||
isPrimType Bits64Type = True
|
||||
isPrimType StringType = True
|
||||
isPrimType CharType = True
|
||||
isPrimType DoubleType = True
|
||||
isPrimType WorldType = True
|
||||
export
|
||||
primTypeEq : (x, y : PrimType) -> Maybe (x = y)
|
||||
primTypeEq IntType IntType = Just Refl
|
||||
primTypeEq Int8Type Int8Type = Just Refl
|
||||
primTypeEq Int16Type Int16Type = Just Refl
|
||||
primTypeEq Int32Type Int32Type = Just Refl
|
||||
primTypeEq Int64Type Int64Type = Just Refl
|
||||
primTypeEq IntegerType IntegerType = Just Refl
|
||||
primTypeEq StringType StringType = Just Refl
|
||||
primTypeEq CharType CharType = Just Refl
|
||||
primTypeEq DoubleType DoubleType = Just Refl
|
||||
primTypeEq WorldType WorldType = Just Refl
|
||||
primTypeEq _ _ = Nothing
|
||||
|
||||
-- TODO : The `TempXY` instances can be removed after the next release
|
||||
-- (see also `Libraries.Data.Primitives`)
|
||||
@ -183,35 +173,13 @@ constantEq (Ch x) (Ch y) = case decEq x y of
|
||||
Yes Refl => Just Refl
|
||||
No contra => Nothing
|
||||
constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
|
||||
constantEq (PrT x) (PrT y) = cong PrT <$> primTypeEq x y
|
||||
constantEq WorldVal WorldVal = Just Refl
|
||||
constantEq IntType IntType = Just Refl
|
||||
constantEq Int8Type Int8Type = Just Refl
|
||||
constantEq Int16Type Int16Type = Just Refl
|
||||
constantEq Int32Type Int32Type = Just Refl
|
||||
constantEq Int64Type Int64Type = Just Refl
|
||||
constantEq IntegerType IntegerType = Just Refl
|
||||
constantEq StringType StringType = Just Refl
|
||||
constantEq CharType CharType = Just Refl
|
||||
constantEq DoubleType DoubleType = Just Refl
|
||||
constantEq WorldType WorldType = Just Refl
|
||||
|
||||
constantEq _ _ = Nothing
|
||||
|
||||
export
|
||||
Show Constant where
|
||||
show (I x) = show x
|
||||
show (I8 x) = show x
|
||||
show (I16 x) = show x
|
||||
show (I32 x) = show x
|
||||
show (I64 x) = show x
|
||||
show (BI x) = show x
|
||||
show (B8 x) = show x
|
||||
show (B16 x) = show x
|
||||
show (B32 x) = show x
|
||||
show (B64 x) = show x
|
||||
show (Str x) = show x
|
||||
show (Ch x) = show x
|
||||
show (Db x) = show x
|
||||
show WorldVal = "%MkWorld"
|
||||
Show PrimType where
|
||||
show IntType = "Int"
|
||||
show Int8Type = "Int8"
|
||||
show Int16Type = "Int16"
|
||||
@ -228,21 +196,25 @@ Show Constant where
|
||||
show WorldType = "%World"
|
||||
|
||||
export
|
||||
Pretty Constant where
|
||||
pretty (I x) = pretty x
|
||||
pretty (I8 x) = pretty x
|
||||
pretty (I16 x) = pretty x
|
||||
pretty (I32 x) = pretty x
|
||||
pretty (I64 x) = pretty x
|
||||
pretty (BI x) = pretty x
|
||||
pretty (B8 x) = pretty x
|
||||
pretty (B16 x) = pretty x
|
||||
pretty (B32 x) = pretty x
|
||||
pretty (B64 x) = pretty x
|
||||
pretty (Str x) = dquotes (pretty x)
|
||||
pretty (Ch x) = squotes (pretty x)
|
||||
pretty (Db x) = pretty x
|
||||
pretty WorldVal = pretty "%MkWorld"
|
||||
Show Constant where
|
||||
show (I x) = show x
|
||||
show (I8 x) = show x
|
||||
show (I16 x) = show x
|
||||
show (I32 x) = show x
|
||||
show (I64 x) = show x
|
||||
show (BI x) = show x
|
||||
show (B8 x) = show x
|
||||
show (B16 x) = show x
|
||||
show (B32 x) = show x
|
||||
show (B64 x) = show x
|
||||
show (Str x) = show x
|
||||
show (Ch x) = show x
|
||||
show (Db x) = show x
|
||||
show (PrT x) = show x
|
||||
show WorldVal = "%MkWorld"
|
||||
|
||||
export
|
||||
Pretty PrimType where
|
||||
pretty IntType = pretty "Int"
|
||||
pretty Int8Type = pretty "Int8"
|
||||
pretty Int16Type = pretty "Int16"
|
||||
@ -259,21 +231,25 @@ Pretty Constant where
|
||||
pretty WorldType = pretty "%World"
|
||||
|
||||
export
|
||||
Eq Constant where
|
||||
(I x) == (I y) = x == y
|
||||
(I8 x) == (I8 y) = x == y
|
||||
(I16 x) == (I16 y) = x == y
|
||||
(I32 x) == (I32 y) = x == y
|
||||
(I64 x) == (I64 y) = x == y
|
||||
(BI x) == (BI y) = x == y
|
||||
(B8 x) == (B8 y) = x == y
|
||||
(B16 x) == (B16 y) = x == y
|
||||
(B32 x) == (B32 y) = x == y
|
||||
(B64 x) == (B64 y) = x == y
|
||||
(Str x) == (Str y) = x == y
|
||||
(Ch x) == (Ch y) = x == y
|
||||
(Db x) == (Db y) = x == y
|
||||
WorldVal == WorldVal = True
|
||||
Pretty Constant where
|
||||
pretty (I x) = pretty x
|
||||
pretty (I8 x) = pretty x
|
||||
pretty (I16 x) = pretty x
|
||||
pretty (I32 x) = pretty x
|
||||
pretty (I64 x) = pretty x
|
||||
pretty (BI x) = pretty x
|
||||
pretty (B8 x) = pretty x
|
||||
pretty (B16 x) = pretty x
|
||||
pretty (B32 x) = pretty x
|
||||
pretty (B64 x) = pretty x
|
||||
pretty (Str x) = dquotes (pretty x)
|
||||
pretty (Ch x) = squotes (pretty x)
|
||||
pretty (Db x) = pretty x
|
||||
pretty (PrT x) = pretty x
|
||||
pretty WorldVal = pretty "%MkWorld"
|
||||
|
||||
export
|
||||
Eq PrimType where
|
||||
IntType == IntType = True
|
||||
Int8Type == Int8Type = True
|
||||
Int16Type == Int16Type = True
|
||||
@ -290,25 +266,43 @@ Eq Constant where
|
||||
WorldType == WorldType = True
|
||||
_ == _ = False
|
||||
|
||||
export
|
||||
Eq Constant where
|
||||
(I x) == (I y) = x == y
|
||||
(I8 x) == (I8 y) = x == y
|
||||
(I16 x) == (I16 y) = x == y
|
||||
(I32 x) == (I32 y) = x == y
|
||||
(I64 x) == (I64 y) = x == y
|
||||
(BI x) == (BI y) = x == y
|
||||
(B8 x) == (B8 y) = x == y
|
||||
(B16 x) == (B16 y) = x == y
|
||||
(B32 x) == (B32 y) = x == y
|
||||
(B64 x) == (B64 y) = x == y
|
||||
(Str x) == (Str y) = x == y
|
||||
(Ch x) == (Ch y) = x == y
|
||||
(Db x) == (Db y) = x == y
|
||||
(PrT x) == (PrT y) = x == y
|
||||
WorldVal == WorldVal = True
|
||||
_ == _ = False
|
||||
|
||||
-- for typecase
|
||||
export
|
||||
constTag : Constant -> Int
|
||||
primTypeTag : PrimType -> Int
|
||||
-- 1 = ->, 2 = Type
|
||||
constTag IntType = 3
|
||||
constTag IntegerType = 4
|
||||
constTag Bits8Type = 5
|
||||
constTag Bits16Type = 6
|
||||
constTag Bits32Type = 7
|
||||
constTag Bits64Type = 8
|
||||
constTag StringType = 9
|
||||
constTag CharType = 10
|
||||
constTag DoubleType = 11
|
||||
constTag WorldType = 12
|
||||
constTag Int8Type = 13
|
||||
constTag Int16Type = 14
|
||||
constTag Int32Type = 15
|
||||
constTag Int64Type = 16
|
||||
constTag _ = 0
|
||||
primTypeTag IntType = 3
|
||||
primTypeTag IntegerType = 4
|
||||
primTypeTag Bits8Type = 5
|
||||
primTypeTag Bits16Type = 6
|
||||
primTypeTag Bits32Type = 7
|
||||
primTypeTag Bits64Type = 8
|
||||
primTypeTag StringType = 9
|
||||
primTypeTag CharType = 10
|
||||
primTypeTag DoubleType = 11
|
||||
primTypeTag WorldType = 12
|
||||
primTypeTag Int8Type = 13
|
||||
primTypeTag Int16Type = 14
|
||||
primTypeTag Int32Type = 15
|
||||
primTypeTag Int64Type = 16
|
||||
|
||||
||| Precision of integral types.
|
||||
public export
|
||||
@ -333,7 +327,7 @@ public export
|
||||
data IntKind = Signed Precision | Unsigned Int
|
||||
|
||||
public export
|
||||
intKind : Constant -> Maybe IntKind
|
||||
intKind : PrimType -> Maybe IntKind
|
||||
intKind IntegerType = Just $ Signed Unlimited
|
||||
intKind Int8Type = Just . Signed $ P 8
|
||||
intKind Int16Type = Just . Signed $ P 16
|
||||
@ -354,24 +348,24 @@ precision (Unsigned p) = P p
|
||||
-- All the internal operators, parameterised by their arity
|
||||
public export
|
||||
data PrimFn : Nat -> Type where
|
||||
Add : (ty : Constant) -> PrimFn 2
|
||||
Sub : (ty : Constant) -> PrimFn 2
|
||||
Mul : (ty : Constant) -> PrimFn 2
|
||||
Div : (ty : Constant) -> PrimFn 2
|
||||
Mod : (ty : Constant) -> PrimFn 2
|
||||
Neg : (ty : Constant) -> PrimFn 1
|
||||
ShiftL : (ty : Constant) -> PrimFn 2
|
||||
ShiftR : (ty : Constant) -> PrimFn 2
|
||||
Add : (ty : PrimType) -> PrimFn 2
|
||||
Sub : (ty : PrimType) -> PrimFn 2
|
||||
Mul : (ty : PrimType) -> PrimFn 2
|
||||
Div : (ty : PrimType) -> PrimFn 2
|
||||
Mod : (ty : PrimType) -> PrimFn 2
|
||||
Neg : (ty : PrimType) -> PrimFn 1
|
||||
ShiftL : (ty : PrimType) -> PrimFn 2
|
||||
ShiftR : (ty : PrimType) -> PrimFn 2
|
||||
|
||||
BAnd : (ty : Constant) -> PrimFn 2
|
||||
BOr : (ty : Constant) -> PrimFn 2
|
||||
BXOr : (ty : Constant) -> PrimFn 2
|
||||
BAnd : (ty : PrimType) -> PrimFn 2
|
||||
BOr : (ty : PrimType) -> PrimFn 2
|
||||
BXOr : (ty : PrimType) -> PrimFn 2
|
||||
|
||||
LT : (ty : Constant) -> PrimFn 2
|
||||
LTE : (ty : Constant) -> PrimFn 2
|
||||
EQ : (ty : Constant) -> PrimFn 2
|
||||
GTE : (ty : Constant) -> PrimFn 2
|
||||
GT : (ty : Constant) -> PrimFn 2
|
||||
LT : (ty : PrimType) -> PrimFn 2
|
||||
LTE : (ty : PrimType) -> PrimFn 2
|
||||
EQ : (ty : PrimType) -> PrimFn 2
|
||||
GTE : (ty : PrimType) -> PrimFn 2
|
||||
GT : (ty : PrimType) -> PrimFn 2
|
||||
|
||||
StrLength : PrimFn 1
|
||||
StrHead : PrimFn 1
|
||||
@ -395,7 +389,7 @@ data PrimFn : Nat -> Type where
|
||||
DoubleFloor : PrimFn 1
|
||||
DoubleCeiling : PrimFn 1
|
||||
|
||||
Cast : Constant -> Constant -> PrimFn 1
|
||||
Cast : PrimType -> PrimType -> PrimFn 1
|
||||
BelieveMe : PrimFn 3
|
||||
Crash : PrimFn 2
|
||||
|
||||
|
||||
122
src/Core/TTC.idr
122
src/Core/TTC.idr
@ -147,69 +147,75 @@ TTC t => TTC (PiInfo t) where
|
||||
3 => do t <- fromBuf b; pure (DefImplicit t)
|
||||
_ => corrupt "PiInfo"
|
||||
|
||||
export
|
||||
TTC PrimType where
|
||||
toBuf b IntType = tag 0
|
||||
toBuf b Int8Type = tag 1
|
||||
toBuf b Int16Type = tag 2
|
||||
toBuf b Int32Type = tag 3
|
||||
toBuf b Int64Type = tag 4
|
||||
toBuf b IntegerType = tag 5
|
||||
toBuf b Bits8Type = tag 6
|
||||
toBuf b Bits16Type = tag 7
|
||||
toBuf b Bits32Type = tag 8
|
||||
toBuf b Bits64Type = tag 9
|
||||
toBuf b StringType = tag 10
|
||||
toBuf b CharType = tag 11
|
||||
toBuf b DoubleType = tag 12
|
||||
toBuf b WorldType = tag 13
|
||||
|
||||
fromBuf b = case !getTag of
|
||||
0 => pure IntType
|
||||
1 => pure Int8Type
|
||||
2 => pure Int16Type
|
||||
3 => pure Int32Type
|
||||
4 => pure Int64Type
|
||||
5 => pure IntegerType
|
||||
6 => pure Bits8Type
|
||||
7 => pure Bits16Type
|
||||
8 => pure Bits32Type
|
||||
9 => pure Bits64Type
|
||||
10 => pure StringType
|
||||
11 => pure CharType
|
||||
12 => pure DoubleType
|
||||
13 => pure WorldType
|
||||
_ => corrupt "PrimType"
|
||||
|
||||
export
|
||||
TTC Constant where
|
||||
toBuf b (I x) = do tag 0; toBuf b x
|
||||
toBuf b (BI x) = do tag 1; toBuf b x
|
||||
toBuf b (B8 x) = do tag 2; toBuf b x
|
||||
toBuf b (B16 x) = do tag 3; toBuf b x
|
||||
toBuf b (B32 x) = do tag 4; toBuf b x
|
||||
toBuf b (B64 x) = do tag 5; toBuf b x
|
||||
toBuf b (Str x) = do tag 6; toBuf b x
|
||||
toBuf b (Ch x) = do tag 7; toBuf b x
|
||||
toBuf b (Db x) = do tag 8; toBuf b x
|
||||
|
||||
toBuf b WorldVal = tag 9
|
||||
toBuf b IntType = tag 10
|
||||
toBuf b IntegerType = tag 11
|
||||
toBuf b Bits8Type = tag 12
|
||||
toBuf b Bits16Type = tag 13
|
||||
toBuf b Bits32Type = tag 14
|
||||
toBuf b Bits64Type = tag 15
|
||||
toBuf b StringType = tag 16
|
||||
toBuf b CharType = tag 17
|
||||
toBuf b DoubleType = tag 18
|
||||
toBuf b WorldType = tag 19
|
||||
|
||||
toBuf b (I32 x) = do tag 20; toBuf b x
|
||||
toBuf b (I64 x) = do tag 21; toBuf b x
|
||||
toBuf b Int32Type = tag 22
|
||||
toBuf b Int64Type = tag 23
|
||||
toBuf b (I8 x) = do tag 24; toBuf b x
|
||||
toBuf b (I16 x) = do tag 25; toBuf b x
|
||||
toBuf b Int8Type = tag 26
|
||||
toBuf b Int16Type = tag 27
|
||||
toBuf b (I x) = do tag 0; toBuf b x
|
||||
toBuf b (I8 x) = do tag 1; toBuf b x
|
||||
toBuf b (I16 x) = do tag 2; toBuf b x
|
||||
toBuf b (I32 x) = do tag 3; toBuf b x
|
||||
toBuf b (I64 x) = do tag 4; toBuf b x
|
||||
toBuf b (BI x) = do tag 5; toBuf b x
|
||||
toBuf b (B8 x) = do tag 6; toBuf b x
|
||||
toBuf b (B16 x) = do tag 7; toBuf b x
|
||||
toBuf b (B32 x) = do tag 8; toBuf b x
|
||||
toBuf b (B64 x) = do tag 9; toBuf b x
|
||||
toBuf b (Str x) = do tag 10; toBuf b x
|
||||
toBuf b (Ch x) = do tag 11; toBuf b x
|
||||
toBuf b (Db x) = do tag 12; toBuf b x
|
||||
toBuf b (PrT x) = do tag 13; toBuf b x
|
||||
toBuf b WorldVal = tag 14
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
0 => do x <- fromBuf b; pure (I x)
|
||||
1 => do x <- fromBuf b; pure (BI x)
|
||||
2 => do x <- fromBuf b; pure (B8 x)
|
||||
3 => do x <- fromBuf b; pure (B16 x)
|
||||
4 => do x <- fromBuf b; pure (B32 x)
|
||||
5 => do x <- fromBuf b; pure (B64 x)
|
||||
6 => do x <- fromBuf b; pure (Str x)
|
||||
7 => do x <- fromBuf b; pure (Ch x)
|
||||
8 => do x <- fromBuf b; pure (Db x)
|
||||
9 => pure WorldVal
|
||||
10 => pure IntType
|
||||
11 => pure IntegerType
|
||||
12 => pure Bits8Type
|
||||
13 => pure Bits16Type
|
||||
14 => pure Bits32Type
|
||||
15 => pure Bits64Type
|
||||
16 => pure StringType
|
||||
17 => pure CharType
|
||||
18 => pure DoubleType
|
||||
19 => pure WorldType
|
||||
20 => do x <- fromBuf b; pure (I32 x)
|
||||
21 => do x <- fromBuf b; pure (I64 x)
|
||||
22 => pure Int32Type
|
||||
23 => pure Int64Type
|
||||
24 => do x <- fromBuf b; pure (I8 x)
|
||||
25 => do x <- fromBuf b; pure (I16 x)
|
||||
26 => pure Int8Type
|
||||
27 => pure Int16Type
|
||||
0 => do x <- fromBuf b; pure (I x)
|
||||
1 => do x <- fromBuf b; pure (I8 x)
|
||||
2 => do x <- fromBuf b; pure (I16 x)
|
||||
3 => do x <- fromBuf b; pure (I32 x)
|
||||
4 => do x <- fromBuf b; pure (I64 x)
|
||||
5 => do x <- fromBuf b; pure (BI x)
|
||||
6 => do x <- fromBuf b; pure (B8 x)
|
||||
7 => do x <- fromBuf b; pure (B16 x)
|
||||
8 => do x <- fromBuf b; pure (B32 x)
|
||||
9 => do x <- fromBuf b; pure (B64 x)
|
||||
10 => do x <- fromBuf b; pure (Str x)
|
||||
11 => do x <- fromBuf b; pure (Ch x)
|
||||
12 => do x <- fromBuf b; pure (Db x)
|
||||
13 => do x <- fromBuf b; pure (PrT x)
|
||||
14 => pure WorldVal
|
||||
_ => corrupt "Constant"
|
||||
|
||||
export
|
||||
|
||||
@ -106,7 +106,7 @@ ntCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars
|
||||
-- universe checking so put a dummy name.
|
||||
ntCon fc (UN (Basic "Type")) tag Z [] = NType fc (MN "top" 0)
|
||||
ntCon fc n tag Z [] = case isConstantType n of
|
||||
Just c => NPrimVal fc c
|
||||
Just c => NPrimVal fc $ PrT c
|
||||
Nothing => NTCon fc n tag Z []
|
||||
ntCon fc n tag arity args = NTCon fc n tag arity args
|
||||
|
||||
|
||||
@ -162,6 +162,22 @@ getDocsForPrimitive constant = do
|
||||
:: hintsDoc
|
||||
|
||||
where
|
||||
primTyDoc : PrimType -> Doc IdrisDocAnn
|
||||
primTyDoc IntType = "Primitive type of bounded signed integers (backend dependent size)"
|
||||
primTyDoc Int8Type = "Primitive type of 8 bits signed integers"
|
||||
primTyDoc Int16Type = "Primitive type of 16 bits signed integers"
|
||||
primTyDoc Int32Type = "Primitive type of 32 bits signed integers"
|
||||
primTyDoc Int64Type = "Primitive type of 64 bits signed integers"
|
||||
primTyDoc IntegerType = "Primitive type of unbounded signed integers"
|
||||
primTyDoc Bits8Type = "Primitive type of 8 bits unsigned integers"
|
||||
primTyDoc Bits16Type = "Primitive type of 16 bits unsigned integers"
|
||||
primTyDoc Bits32Type = "Primitive type of 32 bits unsigned integers"
|
||||
primTyDoc Bits64Type = "Primitive type of 64 bits unsigned integers"
|
||||
primTyDoc StringType = "Primitive type of strings"
|
||||
primTyDoc CharType = "Primitive type of characters"
|
||||
primTyDoc DoubleType = "Primitive type of double-precision floating-points"
|
||||
primTyDoc WorldType = "Primitive type of tokens for IO actions"
|
||||
|
||||
primDoc : Constant -> Doc IdrisDocAnn
|
||||
primDoc (I i) = "Primitive signed int value (backend-dependent precision)"
|
||||
primDoc (I8 i) = "Primitive signed 8 bits value"
|
||||
@ -176,23 +192,9 @@ getDocsForPrimitive constant = do
|
||||
primDoc (Str s) = "Primitive string value"
|
||||
primDoc (Ch c) = "Primitive character value"
|
||||
primDoc (Db d) = "Primitive double value"
|
||||
primDoc (PrT t) = primTyDoc t
|
||||
primDoc WorldVal = "Primitive token for IO actions"
|
||||
|
||||
primDoc IntType = "Primitive type of bounded signed integers (backend dependent size)"
|
||||
primDoc Int8Type = "Primitive type of 8 bits signed integers"
|
||||
primDoc Int16Type = "Primitive type of 16 bits signed integers"
|
||||
primDoc Int32Type = "Primitive type of 32 bits signed integers"
|
||||
primDoc Int64Type = "Primitive type of 64 bits signed integers"
|
||||
primDoc IntegerType = "Primitive type of unbounded signed integers"
|
||||
primDoc Bits8Type = "Primitive type of 8 bits unsigned integers"
|
||||
primDoc Bits16Type = "Primitive type of 16 bits unsigned integers"
|
||||
primDoc Bits32Type = "Primitive type of 32 bits unsigned integers"
|
||||
primDoc Bits64Type = "Primitive type of 64 bits unsigned integers"
|
||||
primDoc StringType = "Primitive type of strings"
|
||||
primDoc CharType = "Primitive type of characters"
|
||||
primDoc DoubleType = "Primitive type of double-precision floating-points"
|
||||
primDoc WorldType = "Primitive type of tokens for IO actions"
|
||||
|
||||
public export
|
||||
data Config : Type where
|
||||
||| Configuration of the printer for a name
|
||||
|
||||
@ -140,7 +140,7 @@ atom fname
|
||||
<|> do x <- bounds $ decorate fname Data $ pragma "MkWorld"
|
||||
pure (PPrimVal (boundToFC fname x) WorldVal)
|
||||
<|> do x <- bounds $ decorate fname Typ $ pragma "World"
|
||||
pure (PPrimVal (boundToFC fname x) WorldType)
|
||||
pure (PPrimVal (boundToFC fname x) $ PrT WorldType)
|
||||
<|> do x <- bounds $ decoratedPragma fname "search"
|
||||
pure (PSearch (boundToFC fname x) 50)
|
||||
|
||||
|
||||
@ -58,44 +58,17 @@ fuzzySearch expr = do
|
||||
where
|
||||
|
||||
data NameOrConst = AName Name
|
||||
| AInt
|
||||
| AInteger
|
||||
| ABits8
|
||||
| ABits16
|
||||
| ABits32
|
||||
| ABits64
|
||||
| AString
|
||||
| AChar
|
||||
| ADouble
|
||||
| AWorld
|
||||
| APrimType PrimType
|
||||
| AType
|
||||
|
||||
eqConst : (x, y : NameOrConst) -> Bool
|
||||
eqConst AInt AInt = True
|
||||
eqConst AInteger AInteger = True
|
||||
eqConst ABits8 ABits8 = True
|
||||
eqConst ABits16 ABits16 = True
|
||||
eqConst ABits32 ABits32 = True
|
||||
eqConst ABits64 ABits64 = True
|
||||
eqConst AString AString = True
|
||||
eqConst AChar AChar = True
|
||||
eqConst ADouble ADouble = True
|
||||
eqConst AWorld AWorld = True
|
||||
eqConst AType AType = True
|
||||
eqConst _ _ = False
|
||||
eqConst (APrimType x) (APrimType y) = x == y
|
||||
eqConst AType AType = True
|
||||
eqConst _ _ = False -- names equality is irrelevant
|
||||
|
||||
parseNameOrConst : PTerm -> Maybe NameOrConst
|
||||
parseNameOrConst (PRef _ n) = Just (AName n)
|
||||
parseNameOrConst (PPrimVal _ IntType) = Just AInt
|
||||
parseNameOrConst (PPrimVal _ IntegerType) = Just AInteger
|
||||
parseNameOrConst (PPrimVal _ Bits8Type) = Just ABits8
|
||||
parseNameOrConst (PPrimVal _ Bits16Type) = Just ABits16
|
||||
parseNameOrConst (PPrimVal _ Bits32Type) = Just ABits32
|
||||
parseNameOrConst (PPrimVal _ Bits64Type) = Just ABits64
|
||||
parseNameOrConst (PPrimVal _ StringType) = Just AString
|
||||
parseNameOrConst (PPrimVal _ CharType) = Just AChar
|
||||
parseNameOrConst (PPrimVal _ DoubleType) = Just ADouble
|
||||
parseNameOrConst (PPrimVal _ WorldType) = Just AWorld
|
||||
parseNameOrConst (PPrimVal _ $ PrT t) = Just (APrimType t)
|
||||
parseNameOrConst (PType _) = Just AType
|
||||
parseNameOrConst _ = Nothing
|
||||
|
||||
|
||||
@ -82,12 +82,12 @@ export
|
||||
constant : Rule Constant
|
||||
constant
|
||||
= terminal "Expected constant" $ \case
|
||||
CharLit c => Ch <$> getCharLit c
|
||||
CharLit c => Ch <$> getCharLit c
|
||||
DoubleLit d => Just (Db d)
|
||||
IntegerLit i => Just (BI i)
|
||||
Ident s => isConstantType (UN $ Basic s) >>=
|
||||
\case WorldType => Nothing
|
||||
c => Just c
|
||||
c => Just $ PrT c
|
||||
_ => Nothing
|
||||
|
||||
documentation' : Rule String
|
||||
|
||||
@ -2,39 +2,22 @@ module TTImp.Elab.Prim
|
||||
|
||||
import Core.TT
|
||||
|
||||
%default covering
|
||||
|
||||
ttype : FC -> Term vars
|
||||
ttype fc = TType fc (MN "top" 0)
|
||||
%default total
|
||||
|
||||
export
|
||||
checkPrim : FC -> Constant -> (Term vars, Term vars)
|
||||
checkPrim fc (I i) = (PrimVal fc (I i), PrimVal fc IntType)
|
||||
checkPrim fc (I8 i) = (PrimVal fc (I8 i), PrimVal fc Int8Type)
|
||||
checkPrim fc (I16 i) = (PrimVal fc (I16 i), PrimVal fc Int16Type)
|
||||
checkPrim fc (I32 i) = (PrimVal fc (I32 i), PrimVal fc Int32Type)
|
||||
checkPrim fc (I64 i) = (PrimVal fc (I64 i), PrimVal fc Int64Type)
|
||||
checkPrim fc (BI i) = (PrimVal fc (BI i), PrimVal fc IntegerType)
|
||||
checkPrim fc (B8 i) = (PrimVal fc (B8 i), PrimVal fc Bits8Type)
|
||||
checkPrim fc (B16 i) = (PrimVal fc (B16 i), PrimVal fc Bits16Type)
|
||||
checkPrim fc (B32 i) = (PrimVal fc (B32 i), PrimVal fc Bits32Type)
|
||||
checkPrim fc (B64 i) = (PrimVal fc (B64 i), PrimVal fc Bits64Type)
|
||||
checkPrim fc (Str s) = (PrimVal fc (Str s), PrimVal fc StringType)
|
||||
checkPrim fc (Ch c) = (PrimVal fc (Ch c), PrimVal fc CharType)
|
||||
checkPrim fc (Db d) = (PrimVal fc (Db d), PrimVal fc DoubleType)
|
||||
checkPrim fc WorldVal = (PrimVal fc WorldVal, PrimVal fc WorldType)
|
||||
|
||||
checkPrim fc IntType = (PrimVal fc IntType, ttype fc)
|
||||
checkPrim fc Int8Type = (PrimVal fc Int8Type, ttype fc)
|
||||
checkPrim fc Int16Type = (PrimVal fc Int16Type, ttype fc)
|
||||
checkPrim fc Int32Type = (PrimVal fc Int32Type, ttype fc)
|
||||
checkPrim fc Int64Type = (PrimVal fc Int64Type, ttype fc)
|
||||
checkPrim fc IntegerType = (PrimVal fc IntegerType, ttype fc)
|
||||
checkPrim fc Bits8Type = (PrimVal fc Bits8Type, ttype fc)
|
||||
checkPrim fc Bits16Type = (PrimVal fc Bits16Type, ttype fc)
|
||||
checkPrim fc Bits32Type = (PrimVal fc Bits32Type, ttype fc)
|
||||
checkPrim fc Bits64Type = (PrimVal fc Bits64Type, ttype fc)
|
||||
checkPrim fc StringType = (PrimVal fc StringType, ttype fc)
|
||||
checkPrim fc CharType = (PrimVal fc CharType, ttype fc)
|
||||
checkPrim fc DoubleType = (PrimVal fc DoubleType, ttype fc)
|
||||
checkPrim fc WorldType = (PrimVal fc WorldType, ttype fc)
|
||||
checkPrim fc (I i) = (PrimVal fc (I i), PrimVal fc $ PrT IntType)
|
||||
checkPrim fc (I8 i) = (PrimVal fc (I8 i), PrimVal fc $ PrT Int8Type)
|
||||
checkPrim fc (I16 i) = (PrimVal fc (I16 i), PrimVal fc $ PrT Int16Type)
|
||||
checkPrim fc (I32 i) = (PrimVal fc (I32 i), PrimVal fc $ PrT Int32Type)
|
||||
checkPrim fc (I64 i) = (PrimVal fc (I64 i), PrimVal fc $ PrT Int64Type)
|
||||
checkPrim fc (BI i) = (PrimVal fc (BI i), PrimVal fc $ PrT IntegerType)
|
||||
checkPrim fc (B8 i) = (PrimVal fc (B8 i), PrimVal fc $ PrT Bits8Type)
|
||||
checkPrim fc (B16 i) = (PrimVal fc (B16 i), PrimVal fc $ PrT Bits16Type)
|
||||
checkPrim fc (B32 i) = (PrimVal fc (B32 i), PrimVal fc $ PrT Bits32Type)
|
||||
checkPrim fc (B64 i) = (PrimVal fc (B64 i), PrimVal fc $ PrT Bits64Type)
|
||||
checkPrim fc (Str s) = (PrimVal fc (Str s), PrimVal fc $ PrT StringType)
|
||||
checkPrim fc (Ch c) = (PrimVal fc (Ch c), PrimVal fc $ PrT CharType)
|
||||
checkPrim fc (Db d) = (PrimVal fc (Db d), PrimVal fc $ PrT DoubleType)
|
||||
checkPrim fc (PrT t) = (PrimVal fc (PrT t), TType fc (MN "top" 0))
|
||||
checkPrim fc WorldVal = (PrimVal fc WorldVal, PrimVal fc $ PrT WorldType)
|
||||
|
||||
@ -93,7 +93,7 @@ getNEIntegerIndex (Bind _ x b tm) = case b of
|
||||
_ => Nothing
|
||||
where
|
||||
isInteger : forall vars. Term vars -> Bool
|
||||
isInteger (PrimVal _ IntegerType) = True
|
||||
isInteger (PrimVal _ $ PrT IntegerType) = True
|
||||
isInteger _ = False
|
||||
getNEIntegerIndex _ = Just []
|
||||
|
||||
|
||||
@ -215,7 +215,7 @@ getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc)
|
||||
-- %World is never inspected, so might as well be deleted from data types,
|
||||
-- although it needs care when compiling to ensure that the function that
|
||||
-- returns the IO/%World type isn't erased
|
||||
(NPrimVal _ WorldType) =>
|
||||
(NPrimVal _ $ PrT WorldType) =>
|
||||
getRelevantArg defs (1 + i) rel False
|
||||
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
|
||||
_ =>
|
||||
|
||||
@ -210,7 +210,7 @@ getFnString (IPrimVal _ (Str st)) = pure st
|
||||
getFnString tm
|
||||
= do inidx <- resolveName (UN $ Basic "[foreign]")
|
||||
let fc = getFC tm
|
||||
let gstr = gnf [] (PrimVal fc StringType)
|
||||
let gstr = gnf [] (PrimVal fc $ PrT StringType)
|
||||
etm <- checkTerm inidx InExpr [] (MkNested []) [] tm gstr
|
||||
defs <- get Ctxt
|
||||
case !(nf defs [] etm) of
|
||||
|
||||
@ -35,7 +35,7 @@ quote:37:1--37:21
|
||||
|
||||
Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN (Basic "+"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (BI 4)))
|
||||
Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN (Basic "+"))) (IVar (MkFC (Virtual Interactive) (0, 6) (0, 10)) (UN (Basic "True")))) (IVar (MkFC (Virtual Interactive) (0, 14) (0, 19)) (UN (Basic "False")))
|
||||
Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (UN (Basic "xfn")) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN (Basic "xfn"))) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN (Basic "the"))) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) IntType)) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994)))))
|
||||
Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (UN (Basic "xfn")) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN (Basic "xfn"))) (IPrimVal EmptyFC (I 99994)))
|
||||
Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (UN (Basic "xfn")) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) (PrT IntType)) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) (PrT IntType)))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN (Basic "xfn"))) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN (Basic "the"))) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) (PrT IntType))) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994)))))
|
||||
Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (UN (Basic "xfn")) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) (PrT IntType)) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) (PrT IntType)))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN (Basic "xfn"))) (IPrimVal EmptyFC (I 99994)))
|
||||
Main> [UN (Basic "names"), NS (MkNS ["Prelude"]) (UN (Basic "+"))]
|
||||
Main> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user