text:
module IdrisJvm.Core.Operator

import IdrisJvm.Core.Asm
import IdrisJvm.Core.Common
import IdrisJvm.Core.Foreign
import IdrisJvm.IR.Types

%access public export

binaryOp : InferredType -> (InferredType -> Asm ()) -> Asm () -> LVar -> LVar -> Asm ()
binaryOp ty ret ops l r = do
  locTypes <- GetFunctionLocTypes
  let lTy = getLocTy locTypes l
  let rTy = getLocTy locTypes r
  loadVar locTypes lTy ty l
  loadVar locTypes rTy ty r
  ops
  ret ty

unaryOp : InferredType -> (InferredType -> Asm ()) -> Asm () -> LVar -> Asm ()
unaryOp ty ret ops x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy ty x
  ops
  ret ty

compareOp : InferredType -> (InferredType -> Asm ()) -> MethodName -> LVar -> LVar -> Asm ()
compareOp ty ret fn l r = do
  locTypes <- GetFunctionLocTypes
  let lTy = getLocTy locTypes l
  let rTy = getLocTy locTypes r
  loadVar locTypes lTy ty l
  loadVar locTypes rTy ty r
  let tyDesc = inferredTypeToFieldTypeDesc ty
  let fnDesc = asmMethodDesc $ MkMethodDescriptor [tyDesc, tyDesc] (FieldDescriptor FieldTyDescBoolean)
  InvokeMethod InvokeStatic utilClass fn fnDesc False
  ret IBool

cgExternalOp : (InferredType -> Asm ()) -> String -> List LVar -> Asm ()
cgExternalOp ret op _ =
  if op == "prim__null"
    then do Aconstnull; ret IUnknown
    else do invokeError $ "OPERATOR " ++ show op ++ " NOT IMPLEMENTED!"; ret IUnknown

lcrash : (InferredType -> Asm ()) -> LVar -> Asm ()
lcrash ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredStringType x
  InvokeMethod InvokeStatic (rtClass "Runtime") "crash" "(Ljava/lang/String;)Ljava/lang/Object;" False
  ret IUnknown

lsystemInfo : (InferredType -> Asm ()) -> LVar -> Asm ()
lsystemInfo ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IInt x
  InvokeMethod InvokeStatic (rtClass "Runtime") "systemInfo" "(I)Ljava/lang/String;" False
  ret inferredStringType

cgOpStrToInt : (InferredType -> Asm ()) -> LVar -> Asm ()
cgOpStrToInt ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredStringType x
  InvokeMethod InvokeStatic "java/lang/Integer" "parseInt" "(Ljava/lang/String;)I" False
  ret IInt

cgOpStrToDouble : (InferredType -> Asm ()) -> LVar -> Asm ()
cgOpStrToDouble ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredStringType x
  InvokeMethod InvokeStatic "java/lang/Double" "parseDouble" "(Ljava/lang/String;)D" False
  ret IDouble

bigIntegerToChar : (InferredType -> Asm ()) -> LVar -> Asm ()
bigIntegerToChar ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredBigIntegerType x
  InvokeMethod InvokeVirtual "java/math/BigInteger" "intValue" "()I" False
  I2c
  ret IChar

intToBigInteger : (InferredType -> Asm ()) -> LVar -> Asm ()
intToBigInteger ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IInt x
  I2l
  InvokeMethod InvokeStatic "java/math/BigInteger" "valueOf"  "(J)Ljava/math/BigInteger;" False
  ret inferredBigIntegerType

bigIntegerToInt : (InferredType -> Asm ()) -> LVar -> Asm ()
bigIntegerToInt ret x = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredBigIntegerType x
  InvokeMethod InvokeVirtual "java/math/BigInteger" "intValue" "()I" False
  ret IInt

longToChar : (InferredType -> Asm ()) -> LVar -> Asm ()
longToChar ret x = do
   locTypes <- GetFunctionLocTypes
   let xTy = getLocTy locTypes x
   loadVar locTypes xTy ILong x
   L2i
   I2c
   ret IChar

longToInt : (InferredType -> Asm ()) -> LVar -> Asm ()
longToInt ret x = do
   locTypes <- GetFunctionLocTypes
   let xTy = getLocTy locTypes x
   loadVar locTypes xTy ILong x
   L2i
   ret IInt

longToBigInteger : (InferredType -> Asm ()) -> LVar -> Asm ()
longToBigInteger ret x = do
   locTypes <- GetFunctionLocTypes
   let xTy = getLocTy locTypes x
   loadVar locTypes xTy ILong x
   InvokeMethod InvokeStatic "java/math/BigInteger" "valueOf"  "(J)Ljava/math/BigInteger;" False
   ret inferredBigIntegerType

intToInt : (InferredType -> Asm ()) -> LVar -> Asm ()
intToInt ret var = do
  locTypes <- GetFunctionLocTypes
  let varTy = getLocTy locTypes var
  loadVar locTypes varTy IInt var
  ret IInt

intToChar : (InferredType -> Asm ()) -> LVar -> Asm ()
intToChar ret x = do
    locTypes <- GetFunctionLocTypes
    let xTy = getLocTy locTypes x
    loadVar locTypes xTy IInt x
    I2c
    ret IChar

intToLong : (InferredType -> Asm ()) -> LVar -> Asm ()
intToLong ret var = do
  locTypes <- GetFunctionLocTypes
  let varTy = getLocTy locTypes var
  loadVar locTypes varTy IInt var
  I2l
  ret ILong

cgOpLLe : (InferredType -> Asm ()) -> IntTy -> List LVar -> Asm ()
cgOpLLe ret ITBig [l, r] = compareOp inferredBigIntegerType ret "bigIntegerLessThanOrEqualTo" l r
cgOpLLe ret ITNative [l, r] = compareOp IInt ret "uintLessThanOrEqualTo" l r
cgOpLLe ret (ITFixed IT8) [l, r] =  compareOp IInt ret "uintLessThanOrEqualTo" l r
cgOpLLe ret (ITFixed IT16) [l, r] = compareOp IInt ret "uintLessThanOrEqualTo" l r
cgOpLLe ret (ITFixed IT32) [l, r] = compareOp IInt ret "uintLessThanOrEqualTo" l r
cgOpLLe ret (ITFixed IT64) [l, r] = compareOp ILong ret "ulongLessThanOrEqualTo" l r

cgOpLLt : (InferredType -> Asm ()) -> IntTy -> List LVar -> Asm ()
cgOpLLt ret ITBig [l, r] = compareOp inferredBigIntegerType ret "bigIntegerLessThan" l r
cgOpLLt ret ITNative [l, r] = compareOp IInt ret "uintLessThan" l r
cgOpLLt ret (ITFixed IT8) [l, r] = compareOp IInt ret "uintLessThan" l r
cgOpLLt ret (ITFixed IT16) [l, r] = compareOp IInt ret "uintLessThan" l r
cgOpLLt ret (ITFixed IT32) [l, r] = compareOp IInt ret "uintLessThan" l r
cgOpLLt ret (ITFixed IT64) [l, r] = compareOp ILong ret "ulongLessThan" l r

cgOpLGt : (InferredType -> Asm ()) -> IntTy -> List LVar -> Asm ()
cgOpLGt ret ITBig [l, r] = compareOp inferredBigIntegerType ret "bigIntegerGreaterThan" l r
cgOpLGt ret ITNative [l, r] = compareOp IInt ret "uintGreaterThan" l r
cgOpLGt ret (ITFixed IT8) [l, r] = compareOp IInt ret "uintGreaterThan" l r
cgOpLGt ret (ITFixed IT16) [l, r] = compareOp IInt ret "uintGreaterThan" l r
cgOpLGt ret (ITFixed IT32) [l, r] = compareOp IInt ret "uintGreaterThan" l r
cgOpLGt ret (ITFixed IT64) [l, r] = compareOp ILong ret "ulongGreaterThan" l r

cgOpLGe : (InferredType -> Asm ()) -> IntTy -> List LVar -> Asm ()
cgOpLGe ret ITBig [l, r] = compareOp inferredBigIntegerType ret "bigIntegerGreaterThanOrEqualTo" l r
cgOpLGe ret ITNative [l, r] = compareOp IInt ret "uintGreaterThanOrEqualTo" l r
cgOpLGe ret (ITFixed IT8) [l, r] = compareOp IInt ret "uintGreaterThanOrEqualTo" l r
cgOpLGe ret (ITFixed IT16) [l, r] = compareOp IInt ret "uintGreaterThanOrEqualTo" l r
cgOpLGe ret (ITFixed IT32) [l, r] = compareOp IInt ret "uintGreaterThanOrEqualTo" l r
cgOpLGe ret (ITFixed IT64) [l, r] = compareOp ILong ret "ulongGreaterThanOrTo" l r

cgOpLPlus : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLPlus ret ATFloat [l, r] = binaryOp IDouble ret Dadd l r
cgOpLPlus ret (ATInt ITBig) [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "add"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar
cgOpLPlus ret (ATInt ITNative) [l, r] = binaryOp IInt ret Iadd l r
cgOpLPlus ret (ATInt ITChar) [lvar, rvar] =
  let ops = do Iadd; I2c
  in binaryOp IChar ret ops lvar rvar
cgOpLPlus ret (ATInt (ITFixed IT64)) [l, r] = binaryOp ILong ret Ladd l r
cgOpLPlus ret (ATInt (ITFixed IT8)) [l, r] =
  let ops = do Iadd; Iconst 256; Irem
  in binaryOp IInt ret ops l r
cgOpLPlus ret (ATInt (ITFixed _)) [l, r] = binaryOp IInt ret Iadd l r

cgOpLMinus : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLMinus ret ATFloat [l, r] = binaryOp IDouble ret Dsub l r
cgOpLMinus ret (ATInt ITBig) [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "subtract"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar
cgOpLMinus ret (ATInt ITNative) [l, r] = binaryOp IInt ret Isub l r
cgOpLMinus ret (ATInt (ITFixed IT64)) [l, r] = binaryOp ILong ret Lsub l r
cgOpLMinus ret (ATInt (ITFixed _)) [l, r] = binaryOp IInt ret Isub l r

cgOpLTimes : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLTimes ret ATFloat [l, r] = binaryOp IDouble ret Dmul l r
cgOpLTimes ret (ATInt ITBig) [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "multiply"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar
cgOpLTimes ret (ATInt ITNative) [l, r] = binaryOp IInt ret Imul l r
cgOpLTimes ret (ATInt (ITFixed IT64)) [l, r] = binaryOp ILong ret Lmul l r
cgOpLTimes ret (ATInt (ITFixed IT8)) [l, r] = binaryOp IInt ret ops l r where
  ops = do Imul; Iconst 256; Irem
cgOpLTimes ret (ATInt (ITFixed _)) [l, r] = binaryOp IInt ret Imul l r

cgOpLSDiv : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLSDiv ret ATFloat [l, r] = binaryOp IDouble ret Ddiv l r
cgOpLSDiv ret (ATInt ITBig) [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "divide"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar
cgOpLSDiv ret (ATInt ITNative) [l, r] = binaryOp IInt ret Idiv l r
cgOpLSDiv ret (ATInt (ITFixed IT64)) [l, r] = binaryOp ILong ret Ldiv l r
cgOpLSDiv ret (ATInt (ITFixed _)) [l, r] = binaryOp IInt ret Idiv l r

cgOpLUDiv : (InferredType -> Asm ()) -> IntTy -> List LVar -> Asm ()
cgOpLUDiv ret ITNative [l, r] = binaryOp IInt ret udiv l r where
  udiv = InvokeMethod InvokeStatic "java/lang/Integer" "divideUnsigned" "(II)I" False
cgOpLUDiv ret (ITFixed IT32) [l, r] = binaryOp IInt ret udiv l r where
  udiv = InvokeMethod InvokeStatic "java/lang/Integer" "divideUnsigned" "(II)I" False
cgOpLUDiv ret (ITFixed IT64) [l, r] = binaryOp ILong ret udiv l r where
  udiv = InvokeMethod InvokeStatic "java/lang/Long" "divideUnsigned" "(JJ)J" False
cgOpLUDiv ret (ITFixed IT16) [l, r] = binaryOp IInt ret udiv l r where
  udiv = InvokeMethod InvokeStatic (rtClass "Bits16s") "divideUnsigned" "(II)I" False
cgOpLUDiv ret (ITFixed IT8) [l, r] = binaryOp IInt ret udiv l r where
  udiv = InvokeMethod InvokeStatic (rtClass "Bits8s") "divideUnsigned" "(II)I" False
cgOpLUDiv ret ITBig [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "divide"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar

cgOpLSRem : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLSRem ret ATFloat [l, r] = binaryOp IDouble ret Drem l r
cgOpLSRem ret (ATInt ITBig) [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "remainder"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar
cgOpLSRem ret (ATInt ITNative) [l, r] = binaryOp IInt ret Irem l r
cgOpLSRem ret (ATInt (ITFixed IT64)) [l, r] = binaryOp ILong ret Lrem l r
cgOpLSRem ret (ATInt (ITFixed _)) [l, r] = binaryOp IInt ret Irem l r

cgOpLURem : (InferredType -> Asm ()) -> IntTy -> List LVar -> Asm ()
cgOpLURem ret (ITFixed IT64) [l, r] = binaryOp ILong ret urem l r where
  urem = InvokeMethod InvokeStatic "java/lang/Long" "remainderUnsigned" "(JJ)J" False
cgOpLURem ret ITNative [l, r] = binaryOp IInt ret urem l r where
  urem = InvokeMethod InvokeStatic "java/lang/Integer" "remainderUnsigned" "(II)I" False
cgOpLURem ret (ITFixed IT32) [l, r] = binaryOp IInt ret urem l r where
  urem = InvokeMethod InvokeStatic "java/lang/Integer" "remainderUnsigned" "(II)I" False
cgOpLURem ret ITBig [lvar, rvar] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "mod"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op lvar rvar
cgOpLURem ret (ITFixed _) [l, r] = binaryOp IInt ret Irem l r

cgOpLEq : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLEq ret ATFloat [l, r] = compareOp IDouble ret "doubleEquals" l r
cgOpLEq ret (ATInt ITBig) [l, r] = compareOp inferredBigIntegerType ret "bigIntegerEquals" l r
cgOpLEq ret (ATInt (ITFixed IT64)) [l, r] = compareOp ILong ret "longEquals" l r
cgOpLEq ret (ATInt ITChar) [l, r] = compareOp IChar ret "charEquals" l r
cgOpLEq ret (ATInt _) [l, r] = compareOp IInt ret "intEquals" l r

cgOpLSLt : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLSLt ret ATFloat [l, r] = compareOp IDouble ret "doubleLessThan" l r
cgOpLSLt ret (ATInt ITNative) [l, r] = compareOp IInt ret "intLessThan" l r
cgOpLSLt ret (ATInt ITBig) [l, r] = compareOp inferredBigIntegerType ret "bigIntegerLessThan" l r
cgOpLSLt ret (ATInt ITChar) [l, r] = compareOp IChar ret "charLessThan" l r
cgOpLSLt ret (ATInt (ITFixed IT64)) [l, r] = compareOp ILong ret "longLessThan" l r
cgOpLSLt ret (ATInt (ITFixed _)) [l, r] = compareOp IInt ret "intLessThan" l r

cgOpLSLe : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLSLe ret ATFloat [l, r] = compareOp IDouble ret "doubleLessThanOrEqualTo" l r
cgOpLSLe ret (ATInt ITNative) [l, r] = compareOp IInt ret "intLessThanOrEqualTo" l r
cgOpLSLe ret (ATInt ITBig) [l, r] = compareOp inferredBigIntegerType ret "bigIntegerLessThanOrEqualTo" l r
cgOpLSLe ret (ATInt ITChar) [l, r] = compareOp IChar ret "charLessThanOrEqualTo" l r
cgOpLSLe ret (ATInt (ITFixed IT64)) [l, r] = compareOp ILong ret "longLessThanOrEqualTo" l r
cgOpLSLe ret (ATInt (ITFixed _)) [l, r] = compareOp IInt ret "intLessThanOrEqualTo" l r

cgOpLSGt : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLSGt ret ATFloat [l, r] = compareOp IDouble ret "doubleGreaterThan" l r
cgOpLSGt ret (ATInt ITNative) [l, r] = compareOp IInt ret "intGreaterThan" l r
cgOpLSGt ret (ATInt ITBig) [l, r] = compareOp inferredBigIntegerType ret "bigIntegerGreaterThan" l r
cgOpLSGt ret (ATInt ITChar) [l, r] = compareOp IChar ret "charGreaterThan" l r
cgOpLSGt ret (ATInt (ITFixed IT64)) [l, r] = compareOp ILong ret "longGreaterThan" l r
cgOpLSGt ret (ATInt (ITFixed _)) [l, r] = compareOp IInt ret "intGreaterThan" l r

cgOpLSGe : (InferredType -> Asm ()) -> ArithTy -> List LVar -> Asm ()
cgOpLSGe ret ATFloat [l, r] = compareOp IDouble ret "doubleGreaterThanOrEqualTo" l r
cgOpLSGe ret (ATInt ITNative) [l, r] = compareOp IInt ret "intGreaterThanOrEqualTo" l r
cgOpLSGe ret (ATInt ITBig) [l, r] = compareOp inferredBigIntegerType ret "bigIntegerGreaterThanOrEqualTo" l r
cgOpLSGe ret (ATInt ITChar) [l, r] = compareOp IChar ret "charGreaterThanOrEqualTo" l r
cgOpLSGe ret (ATInt (ITFixed IT64)) [l, r] = compareOp ILong ret "longGreaterThanOrEqualTo" l r
cgOpLSGe ret (ATInt (ITFixed _)) [l, r] = compareOp IInt ret "intGreaterThanOrEqualTo" l r

cgOpLZExt : (InferredType -> Asm ()) -> IntTy -> IntTy -> List LVar -> Asm ()
cgOpLZExt ret ITNative ITBig [var] = intToBigInteger ret var
cgOpLZExt ret (ITFixed IT64) ITBig [var] = longToBigInteger ret var
cgOpLZExt ret (ITFixed from) ITBig [var] = intToBigInteger ret var

cgOpLZExt ret (ITFixed from) (ITFixed IT64) [var] = intToLong ret var
cgOpLZExt ret ITNative (ITFixed IT64) [var] = intToLong ret var
cgOpLZExt ret ITChar (ITFixed IT64) [var] = intToLong ret var

cgOpLZExt ret ITNative (ITFixed to) [var] = intToInt ret var
cgOpLZExt ret (ITFixed IT64) ITNative [var] = longToInt ret var
cgOpLZExt ret (ITFixed from) ITNative [var] = intToInt ret var
cgOpLZExt ret ITChar ITNative [var] = intToInt ret var
cgOpLZExt ret ITChar (ITFixed to) [var] = intToInt ret var

cgOpLZExt ret (ITFixed IT64) ITChar [var] = longToChar ret var
cgOpLZExt ret (ITFixed from) ITChar [var] = intToChar ret var

cgOpLStrRev : (InferredType -> Asm ()) -> LVar -> Asm ()
cgOpLStrRev ret var = do
  New "java/lang/StringBuilder"
  Dup
  locTypes <- GetFunctionLocTypes
  let varTy = getLocTy locTypes var
  loadVar locTypes varTy inferredStringType var
  InvokeMethod InvokeSpecial "java/lang/StringBuilder" "<init>" "(Ljava/lang/String;)V" False
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "reverse" "()Ljava/lang/StringBuilder;" False
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "toString" "()Ljava/lang/String;" False
  ret inferredStringType

cgOpLStrLen : (InferredType -> Asm ()) -> LVar -> Asm ()
cgOpLStrLen ret var = do
  locTypes <- GetFunctionLocTypes
  let varTy = getLocTy locTypes var
  loadVar locTypes varTy inferredStringType var
  InvokeMethod InvokeVirtual "java/lang/String" "length" "()I" False
  ret IInt

cgOpLStrHead : (InferredType -> Asm ()) -> LVar -> Asm ()
cgOpLStrHead ret var = do
  locTypes <- GetFunctionLocTypes
  let varTy = getLocTy locTypes var
  loadVar locTypes varTy inferredStringType var
  InvokeMethod InvokeStatic (rtClass "Strings") "strHead" "(Ljava/lang/String;)C" False
  ret IChar

cgOpLStrIndex : (InferredType -> Asm ()) -> LVar -> LVar -> Asm ()
cgOpLStrIndex ret string index = do
  locTypes <- GetFunctionLocTypes
  let stringTy = getLocTy locTypes string
  loadVar locTypes stringTy inferredStringType string
  let indexTy = getLocTy locTypes index
  loadVar locTypes indexTy IInt index
  InvokeMethod InvokeStatic (rtClass "Strings") "strIndex" "(Ljava/lang/String;I)C" False
  ret IChar

cgOpLStrTail : (InferredType -> Asm ()) -> LVar -> Asm ()
cgOpLStrTail ret var = do
  locTypes <- GetFunctionLocTypes
  let varTy = getLocTy locTypes var
  loadVar locTypes varTy inferredStringType var
  Iconst 1
  InvokeMethod InvokeVirtual "java/lang/String" "substring" "(I)Ljava/lang/String;" False
  ret inferredStringType

cgOpLStrConcat : (InferredType -> Asm ()) -> LVar -> LVar -> Asm ()
cgOpLStrConcat ret l r = do
  New "java/lang/StringBuilder"
  Dup
  InvokeMethod InvokeSpecial "java/lang/StringBuilder" "<init>" "()V" False
  locTypes <- GetFunctionLocTypes
  let lTy = getLocTy locTypes l
  loadVar locTypes lTy inferredStringType l
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "append" "(Ljava/lang/String;)Ljava/lang/StringBuilder;" False
  let rTy = getLocTy locTypes r
  loadVar locTypes rTy inferredStringType r
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "append" "(Ljava/lang/String;)Ljava/lang/StringBuilder;" False
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "toString" "()Ljava/lang/String;" False
  ret inferredStringType

cgOpLStrCons : (InferredType -> Asm ()) -> LVar -> LVar -> Asm ()
cgOpLStrCons ret l r = do
  New "java/lang/StringBuilder"
  Dup
  InvokeMethod InvokeSpecial "java/lang/StringBuilder" "<init>" "()V" False
  locTypes <- GetFunctionLocTypes
  let lTy = getLocTy locTypes l
  loadVar locTypes lTy IChar l
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "append" "(C)Ljava/lang/StringBuilder;" False
  let rTy = getLocTy locTypes r
  loadVar locTypes rTy inferredStringType r
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "append" "(Ljava/lang/String;)Ljava/lang/StringBuilder;" False
  InvokeMethod InvokeVirtual "java/lang/StringBuilder" "toString" "()Ljava/lang/String;" False
  ret inferredStringType

cgOpLStrSubstr : (InferredType -> Asm ()) -> LVar -> LVar -> LVar -> Asm ()
cgOpLStrSubstr ret offset len str = do
  locTypes <- GetFunctionLocTypes
  let strTy = getLocTy locTypes str
  loadVar locTypes strTy inferredStringType str
  let offsetTy = getLocTy locTypes offset
  loadVar locTypes offsetTy IInt offset
  let lenTy = getLocTy locTypes len
  loadVar locTypes lenTy IInt len
  InvokeMethod InvokeStatic (rtClass "Runtime") "substring" "(Ljava/lang/String;II)Ljava/lang/String;" False
  ret inferredStringType

cgOpBigIntegerUnaryIntOp : (InferredType -> Asm ()) -> Asm () -> LVar -> LVar -> Asm ()
cgOpBigIntegerUnaryIntOp ret op x y = do
  locTypes <- GetFunctionLocTypes
  let lTy = getLocTy locTypes x
  let rTy = getLocTy locTypes y
  loadVar locTypes lTy inferredBigIntegerType x
  loadVar locTypes rTy IInt y
  op
  ret inferredBigIntegerType

cgOpNotImplemented : PrimFn -> Asm ()
cgOpNotImplemented op = invokeError $ "OPERATOR " ++ show op ++ " NOT IMPLEMENTED!"

-- cgOp split into two to avoid JVM's "Method code too large" error.
cgOp2 : (InferredType -> Asm ()) -> PrimFn -> List LVar -> Asm ()
cgOp2 ret (LIntStr ITBig) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredBigIntegerType x
  InvokeMethod InvokeVirtual "java/math/BigInteger" "toString" "()Ljava/lang/String;" False
  ret inferredStringType

cgOp2 ret (LIntStr (ITFixed IT64)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy ILong x
  InvokeMethod InvokeStatic "java/lang/Long" "toUnsignedString" "(J)Ljava/lang/String;" False
  ret inferredStringType

cgOp2 ret (LIntStr _) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IInt x
  InvokeMethod InvokeStatic "java/lang/Integer" "toString" "(I)Ljava/lang/String;" False
  ret inferredStringType

cgOp2 ret LFloatStr [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IDouble x
  InvokeMethod InvokeStatic (rtClass "Doubles") "toString" "(D)Ljava/lang/String;" False
  ret inferredStringType

cgOp2 ret (LChInt ITBig) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IChar x
  I2l
  InvokeMethod InvokeStatic "java/math/BigInteger" "valueOf"  "(J)Ljava/math/BigInteger;" False
  ret inferredBigIntegerType

cgOp2 ret (LChInt (ITFixed IT64)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IChar x
  I2l
  ret ILong

cgOp2 ret (LChInt _) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IChar x
  ret IInt

cgOp2 ret (LIntCh ITBig) [x] = bigIntegerToChar ret x

cgOp2 ret (LIntCh (ITFixed IT64)) [x] = longToChar ret x

cgOp2 ret (LIntCh _) [x] = intToChar ret x

cgOp2 ret (LSExt ITNative ITBig) [x] = intToBigInteger ret x

cgOp2 ret (LSExt (ITFixed IT64) ITBig) [x] = longToBigInteger ret x

cgOp2 ret (LSExt (ITFixed _) ITBig) [x] = intToBigInteger ret x

cgOp2 ret (LTrunc ITNative (ITFixed IT64)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IInt x
  I2l
  ret ILong

cgOp2 ret (LTrunc (ITFixed IT64) (ITFixed _)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy ILong x
  L2i
  ret IInt

cgOp2 ret (LTrunc ITBig (ITFixed IT64)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredBigIntegerType x
  InvokeMethod InvokeVirtual "java/math/BigInteger" "longValue" "()J" False
  ret ILong

cgOp2 ret (LTrunc ITBig (ITFixed _)) [x] = bigIntegerToInt ret x

cgOp2 ret (LTrunc ITBig ITNative) [x] = bigIntegerToInt ret x

cgOp2 ret (LTrunc (ITFixed _) (ITFixed _)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IInt x
  ret IInt

cgOp2 ret LWriteStr [_, x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredStringType x
  InvokeMethod InvokeStatic (rtClass "Runtime") "writeString" "(Ljava/lang/String;)I" False
  ret IInt

cgOp2 ret LReadStr [_] = do
  InvokeMethod InvokeStatic (rtClass "Runtime") "readString" "()Ljava/lang/String;" False
  ret inferredStringType

cgOp2 ret LStrConcat [l,r] = cgOpLStrConcat ret l r

cgOp2 ret LStrCons [l,r] = cgOpLStrCons ret l r

cgOp2 ret LStrSubstr [offset, len, str] = cgOpLStrSubstr ret offset len str

cgOp2 ret (LStrInt ITBig) [x] = do
  New "java/math/BigInteger"
  Dup
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredStringType x
  InvokeMethod InvokeSpecial "java/math/BigInteger" "<init>" "(Ljava/lang/String;)V" False
  ret inferredBigIntegerType

cgOp2 ret (LStrInt (ITFixed IT8)) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredStringType x
  Iconst 16
  InvokeMethod InvokeStatic "java/lang/Integer" "parseInt" "(Ljava/lang/String;I)I" False
  ret IInt

cgOp2 ret (LStrInt _) [x] = cgOpStrToInt ret x

cgOp2 ret LStrFloat [x] = cgOpStrToDouble ret x

cgOp2 ret (LSHL (ITFixed IT64)) [x, y] = binaryOp ILong ret ops x y where
  ops = do L2i; Lshl

cgOp2 ret (LSHL (ITFixed IT8)) [x, y] = binaryOp IInt ret ops x y where
  ops = do Ishl; Iconst 256; Irem

cgOp2 ret (LSHL (ITFixed _)) [x, y] = binaryOp IInt ret Ishl x y

cgOp2 ret (LSHL ITBig) [x, y] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "shiftLeft" "(I)Ljava/math/BigInteger;" False
  in cgOpBigIntegerUnaryIntOp ret op x y

cgOp2 ret (LLSHR (ITFixed IT64)) [x, y] = binaryOp ILong ret ops x y where
  ops = do L2i; Lushr

cgOp2 ret (LLSHR (ITFixed _)) [x, y] = binaryOp IInt ret Iushr x y

cgOp2 ret (LLSHR ITBig) [x, y] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "shiftRight" "(I)Ljava/math/BigInteger;" False
  in cgOpBigIntegerUnaryIntOp ret op x y

cgOp2 ret (LASHR (ITFixed IT64)) [x, y] = binaryOp ILong ret ops x y where
  ops = do L2i; Lshr

cgOp2 ret (LASHR (ITFixed _)) [x, y] = binaryOp IInt ret Ishr x y

cgOp2 ret (LASHR ITBig) [x, y] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "shiftRight" "(I)Ljava/math/BigInteger;" False
  in cgOpBigIntegerUnaryIntOp ret op x y

cgOp2 ret LFork [x] = do
  caller <- GetFunctionName
  createThunk caller (jname "{EVAL_0}") [x]
  InvokeMethod InvokeStatic (rtClass "Concurrent") "fork" ("(" ++ rtThunkSig ++ ")" ++ classSig futureClass) False
  ret (Ref futureClass)

cgOp2 ret LPar [x] = do
  caller <- GetFunctionName
  createParThunk caller (jname "{EVAL_0}") [x]
  InvokeMethod InvokeStatic (rtClass "Concurrent") "par" ("(" ++ rtThunkSig ++ ")" ++ classSig objectClass) False
  ret (Ref objectClass)

cgOp2 ret (LIntFloat ITBig) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy inferredBigIntegerType x
  InvokeMethod InvokeVirtual "java/math/BigInteger" "doubleValue" "()D" False
  ret IDouble

cgOp2 ret (LIntFloat ITNative) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IInt x
  I2d
  ret IDouble

cgOp2 ret (LFloatInt ITBig) [x] = do
  New "java/math/BigDecimal"
  Dup
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IDouble x
  InvokeMethod InvokeSpecial "java/math/BigDecimal" "<init>" "(D)V" False
  InvokeMethod InvokeVirtual "java/math/BigDecimal" "toBigInteger" "()Ljava/math/BigInteger;" False
  ret inferredBigIntegerType

cgOp2 ret (LFloatInt ITNative) [x] = do
  locTypes <- GetFunctionLocTypes
  let xTy = getLocTy locTypes x
  loadVar locTypes xTy IDouble x
  D2i
  ret IInt

cgOp2 ret LSystemInfo [x] = lsystemInfo ret x

cgOp2 ret LCrash [x] = lcrash ret x

cgOp2 ret (LExternal externalOp) args = cgExternalOp ret externalOp args

cgOp2 ret op _ = do cgOpNotImplemented op; ret IUnknown

cgOp : (InferredType -> Asm ()) -> PrimFn -> List LVar -> Asm ()
cgOp ret (LAnd (ITFixed IT64)) [l, r] = binaryOp ILong ret Land l r
cgOp ret (LAnd (ITFixed _)) [l, r] = binaryOp IInt ret Iand l r
cgOp ret (LAnd ITNative) [l, r] = binaryOp IInt ret Iand l r
cgOp ret (LAnd ITBig) [l, r] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "and"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op l r

cgOp ret (LOr (ITFixed IT64)) [l, r] = binaryOp ILong ret Lor l r
cgOp ret (LOr (ITFixed _)) [l, r] = binaryOp IInt ret Ior l r
cgOp ret (LOr ITNative) [l, r] = binaryOp IInt ret Ior l r
cgOp ret (LOr ITBig) [l, r] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "or"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op l r

cgOp ret (LXOr (ITFixed IT64)) [l, r] = binaryOp ILong ret Lxor l r
cgOp ret (LXOr (ITFixed _)) [l, r] = binaryOp IInt ret Ixor l r
cgOp ret (LXOr ITNative) [l, r] = binaryOp IInt ret Ixor l r
cgOp ret (LXOr ITBig) [l, r] =
  let op = InvokeMethod InvokeVirtual "java/math/BigInteger" "xor"  "(Ljava/math/BigInteger;)Ljava/math/BigInteger;" False
  in binaryOp inferredBigIntegerType ret op l r

cgOp ret (LCompl (ITFixed IT64)) [x] = unaryOp ILong ret Lcompl x
cgOp ret (LCompl (ITFixed _)) [x] = unaryOp IInt ret Icompl x
cgOp ret (LCompl ITNative) [x] = unaryOp IInt ret Icompl x

cgOp ret (LLt intTy) args = cgOpLLt ret intTy args

cgOp ret (LLe intTy) args = cgOpLLe ret intTy args

cgOp ret (LGt intTy) args = cgOpLGt ret intTy args

cgOp ret (LGe intTy) args = cgOpLGe ret intTy args

cgOp ret (LPlus arithTy) args = cgOpLPlus ret arithTy args

cgOp ret (LMinus arithTy) args = cgOpLMinus ret arithTy args

cgOp ret (LTimes arithTy) args = cgOpLTimes ret arithTy args

cgOp ret (LSDiv arithTy) args = cgOpLSDiv ret arithTy args

cgOp ret (LUDiv arithTy) args = cgOpLUDiv ret arithTy args

cgOp ret (LSRem arithTy) args = cgOpLSRem ret arithTy args

cgOp ret (LURem intTy) args = cgOpLURem ret intTy args

cgOp ret (LEq arithTy) args = cgOpLEq ret arithTy args

cgOp ret (LSLt arithTy) args = cgOpLSLt ret arithTy args

cgOp ret (LSLe arithTy) args = cgOpLSLe ret arithTy args

cgOp ret (LSGt arithTy) args = cgOpLSGt ret arithTy args

cgOp ret (LSGe arithTy) args = cgOpLSGe ret arithTy args

cgOp ret LStrEq [l,r] = compareOp inferredStringType ret "stringEquals" l r

cgOp ret LStrRev [var] = cgOpLStrRev ret var

cgOp ret LStrLen [var] = cgOpLStrLen ret var

cgOp ret LStrLt [l, r] = compareOp inferredStringType ret "stringLessThan" l r

cgOp ret LStrHead [var] = cgOpLStrHead ret var

cgOp ret LStrIndex [string, index] = cgOpLStrIndex ret string index

cgOp ret LStrTail [var] = cgOpLStrTail ret var

cgOp ret (LZExt from to) args = cgOpLZExt ret from to args

cgOp ret op args = cgOp2 ret op args


text:
{-
  An embeded DSL for prolog-style logic programming, based on the
  pure-prolog parser and interpreter originally written in Haskell

  Original author: Ken Friis Larsen      <kflarsen@diku.dk>
  Translated into Idris by Nathan Bedell <nbedell@tulane.edu>
-}

module Ast

import Data.List

----------------------------------------------------------------------
-- Abstract Syntax Tree
----------------------------------------------------------------------

public export
Atom : Type
Atom = String

public export
Variable : Type
Variable = String

public export
data Term : Type where
 Var : Variable -> Term
 Comp : Atom -> (args: List Term) -> Term

public export
and' : (l : List Bool) -> Bool
and' xs = foldr p True xs
  where
    p : Bool -> Bool -> Bool
    p True True = True
    p x y = False

public export
implementation Eq Term where
  (Var x) == (Var y) = assert_total $ x == y
  (Comp x y) == (Comp x' y') = assert_total $ (x == x') && (and' $ zipWith (==) y y')
  x == y = assert_total $ False

public export
implementation Show Term where
  show (Var s) = s
  show (Comp s []) = s
  show (Comp s xs) = s ++ "(" ++ (concat $ intersperse "," (map (\x => show (assert_smaller xs x)) xs)) ++ ")"

public export
Terms : Type
Terms = List Term

public export
Clause : Type
Clause = (Term, Terms) -- head and body

public export
Clauses : Type
Clauses = List Clause

public export
Goal : Type
Goal = List Term

public export
Program : Type
Program = Clauses

ext: idr


text:
module Text.WebIDL.Codegen.Util

import Data.List
import Data.Nat
import Data.Stream
import public Data.String
import public Data.Vect
import public Text.PrettyPrint.Prettyprinter
import public Text.WebIDL.Codegen.Types
import public Text.WebIDL.Types

export
mapFirstChar : (Char -> Char) -> String -> String
mapFirstChar f x = case fastUnpack x of
                        []       => ""
                        (h :: t) => fastPack (f h :: t)

--------------------------------------------------------------------------------
--          Pretty Utils
--------------------------------------------------------------------------------

export %inline
pretty' : Pretty a => a -> Doc ()
pretty' = pretty

export %inline
prettyPrec' : Pretty a => Prec -> a -> Doc ()
prettyPrec' = prettyPrec

--------------------------------------------------------------------------------
--          Sorted Lists
--------------------------------------------------------------------------------

export
sortedNubOn : Ord b => (a -> b) -> List a -> List a
sortedNubOn f = nub . sortBy (comparing f)
  where nub : List a -> List a
        nub (x :: t@(y :: ys)) = if f x == f y then nub t else x :: nub t
        nub xs                 = xs

export
prettyList : List (Doc ann) -> Doc ann
prettyList []        = "[]"
prettyList (x :: xs) = align $ sep $  ("[" <++> x)
                                   :: map ("," <++>) xs
                                   ++ ["]"]

--------------------------------------------------------------------------------
--          Modules
--------------------------------------------------------------------------------

export
moduleName : String -> String
moduleName "uievents" = "UIEvents"
moduleName s          = mapFirstChar toUpper s

--------------------------------------------------------------------------------
--          String Literals
--------------------------------------------------------------------------------

export
unquote : String -> List Char
unquote = run . fastUnpack
  where run : List Char -> List Char
        run []                   = []
        run ('\\' :: '"' :: cs)  = '"' :: run cs
        run ('"' :: cs)          = run cs
        run (c   :: cs)          = c :: run cs

||| Generates a data constructor from a string literal.
||| This is used for enums, where some values are not
||| valid idris identifiers. Some necessary adjustments
||| are hardcoded here.
export
toDataConstructor : String -> String
toDataConstructor s =
  case unquote s of
       []        => "Empty"
       ['2','d'] => "TwoD"
       c :: cs => fastPack (toUpper c :: run cs)

  where run : List Char -> List Char
        run []             = []
        run (x :: c :: cs) =
          if isAlphaNum x then x :: run (c :: cs) else toUpper c :: run cs
        run (c :: cs)      = c :: run cs

--------------------------------------------------------------------------------
--          Comments
--------------------------------------------------------------------------------

export
title : String -> String
title n = #"""
          --------------------------------------------------------------------------------
          --          \#{n}
          --------------------------------------------------------------------------------
          """#

export
section : String -> List String -> String
section _ Nil = ""
section t ds = fastUnlines ("" :: title t :: ds)

--------------------------------------------------------------------------------
--          Namespaces Implementations
--------------------------------------------------------------------------------

export
namespaced : Identifier -> List String -> String
namespaced _ [] = ""
namespaced n ds = fastUnlines $ "" :: #"namespace \#{n.value}"# :: ds

--------------------------------------------------------------------------------
--          Generating Functions
--------------------------------------------------------------------------------

export
functionTypeOnly : (res : Doc ()) -> (args : List $ Doc ()) -> Doc()
functionTypeOnly res []       = parens $ "() ->" <++> res
functionTypeOnly res (h :: t) =
  let h' = "(" <++> flatAlt (" "  <+> h) h
      args = h' :: map ("->" <++>) (t ++ [res]) ++ [")"]
   in align (sep args)

export
functionTypeWithImplicits :  (name : IdrisIdent)
                          -> (sep : Char)
                          -> (res : Doc ())
                          -> (iargs : List $ Doc ())
                          -> (args : List $ Doc ())
                          -> Doc ()
functionTypeWithImplicits n c res [] [] =
  hsep [pretty n, pretty c, res]

functionTypeWithImplicits n c res [] (h :: t) =
  let h' = pretty c <++> flatAlt (" "  <+> h) h
      args = h' :: map ("->" <++>) (t ++ [res])
   in pretty n <++> align (sep args)

functionTypeWithImplicits n c res (h :: t) [] =
  let h' = pretty c <++> flatAlt (" "  <+> h) h
      args = h' :: map ("=>" <++>) (t ++ [res])
   in pretty n <++> align (sep args)

functionTypeWithImplicits n c res (x :: xs) (y :: ys) =
  let x' = pretty c <++> flatAlt (" "  <+> x) x
      args = x' :: map ("=>" <++>) (xs ++ [y])
                ++ map ("->" <++>) (ys ++ [res])

   in pretty n <++> align (sep args)

export
functionType :  (name : IdrisIdent)
             -> (sep : Char)
             -> (res : Doc ())
             -> (args : List $ Doc ())
             -> Doc ()
functionType n c res = functionTypeWithImplicits n c res []

export
typeDeclWithImplicits :  (name : IdrisIdent)
                      -> (res : Doc ())
                      -> (iargs : List $ Doc ())
                      -> (args : List $ Doc ())
                      -> Doc ()
typeDeclWithImplicits n = functionTypeWithImplicits n ':'

export
typeDecl : (name : IdrisIdent) -> (res : Doc ()) -> (args : List $ Doc ()) -> Doc ()
typeDecl n = functionType n ':'

--------------------------------------------------------------------------------
--          Function Application
--------------------------------------------------------------------------------

export
prettyParens : (b : Bool) -> Doc ann -> Doc ann
prettyParens True  = parens
prettyParens False = id

export
prettyCon : Prec -> (con : Doc ann) -> (args : List (Doc ann)) -> Doc ann
prettyCon p con args = prettyParens (p >= App) (con <++> align (sep args))

--------------------------------------------------------------------------------
--          Function Names
--------------------------------------------------------------------------------

ix : Nat -> String
ix Z = ""
ix k = show k

export
primSetter : Nat -> IdrisIdent
primSetter k = Prim . fromString $ "set" ++ ix k

export
setter : Nat -> IdrisIdent
setter k = fromString $ "set" ++ ix k

export
primGetter : Nat -> IdrisIdent
primGetter k = Prim . fromString $ "get" ++ ix k

export
getter : Nat -> IdrisIdent
getter k = fromString $ "get" ++ ix k

export
primAttrSetter : Nat -> AttributeName -> IdrisIdent
primAttrSetter k n =
  Prim $ fromString ("set" ++ mapFirstChar toUpper n.value ++ ix k)

export
attrSetter : Nat -> AttributeName -> IdrisIdent
attrSetter k n = fromString $ "set" ++ mapFirstChar toUpper n.value ++ ix k

export
primAttrGetter : Nat -> AttributeName -> IdrisIdent
primAttrGetter k n = Prim $ fromString (n.value ++ ix k)

export
attrGetter : Nat -> AttributeName -> IdrisIdent
attrGetter k n = fromString $ n.value ++ ix k

export
primOp : Nat -> OperationName -> IdrisIdent
primOp k n = Prim $ fromString (n.value ++ ix k)

export
op : Nat -> OperationName -> IdrisIdent
op k n = fromString (n.value ++ ix k)

export
primConstr : Nat -> IdrisIdent
primConstr k = Prim $ fromString ("new" ++ ix k)

export
constr : Nat -> IdrisIdent
constr k = fromString ("new" ++ ix k)

export
marshallCallback : Identifier -> IdrisIdent
marshallCallback i = fromString $ "to" ++ i.value

export
primMarshallCallback : Identifier -> IdrisIdent
primMarshallCallback i = Prim . fromString $ "to" ++ i.value

--------------------------------------------------------------------------------
--          Foreign Function Implementations
--------------------------------------------------------------------------------

export
argNames : Stream String
argNames = "a" :: "b" :: "c" :: "d" :: "e" :: "f" :: "g" ::
           "h" :: "i" :: "j" :: "k" :: "l" :: "m" :: "n" ::
           "o" :: "p" :: "q" :: "r" :: "s" :: "t" :: "u" ::
           "v" :: "w" :: "y" :: "z" ::
           map (\v => "x" ++ show v) [the Integer 1 ..]

export
unShadowingArgNames : IdrisIdent -> Stream String
unShadowingArgNames i = go (show i) argNames
  where go : String -> Stream String -> Stream String
        go s (h :: t) = if s == h then t else h :: go s t

foreignBrowser : String -> String
foreignBrowser s = "%foreign \"browser:lambda:" ++ s ++ "\""

export
attrGetFFI : AttributeName -> String
attrGetFFI n = foreignBrowser #"x=>x.\#{n.value}"#

export
staticAttrGetFFI : Kind -> AttributeName -> String
staticAttrGetFFI o n =
  foreignBrowser #"()=>\#{kindToString o}.\#{n.value}"#

export
attrSetFFI : AttributeName -> String
attrSetFFI n = foreignBrowser #"(x,v)=>{x.\#{n.value} = v}"#

export
staticAttrSetFFI : Kind -> AttributeName -> String
staticAttrSetFFI o n =
  foreignBrowser #"v=>{\#{kindToString o}.\#{n.value} = v}"#

export
funFFI : OperationName -> Nat -> String
funFFI n Z = foreignBrowser #"x=>x.\#{n.value}()"#
funFFI n k =
  let vs = take k argNames
      vals = fastConcat $ intersperse "," vs
   in foreignBrowser #"(x,\#{vals})=>x.\#{n.value}(\#{vals})"#

export
funFFIVarArg : OperationName -> Nat -> String
funFFIVarArg n k =
  let vs = take (pred k) argNames
      vals = fastConcat $ intersperse "," (vs ++ ["va"])
      args = fastConcat $ intersperse "," (vs ++ ["...va()"])
   in foreignBrowser #"(x,\#{vals})=>x.\#{n.value}(\#{args})"#

export
staticFunFFI : Kind -> OperationName -> Nat -> String
staticFunFFI o n Z = foreignBrowser #"x=>x.\#{n.value}()"#
staticFunFFI o n k =
  let vs = take k argNames
      vals = fastConcat $ intersperse "," vs
   in foreignBrowser #"(\#{vals})=>\#{kindToString o}.\#{n.value}(\#{vals})"#

export
staticFunFFIVarArg : Kind -> OperationName -> Nat -> String
staticFunFFIVarArg o n k =
  let vs = take (pred k) argNames
      vals = fastConcat $ intersperse "," (vs ++ ["va"])
      args = fastConcat $ intersperse "," (vs ++ ["...va()"])
   in foreignBrowser #"(\#{vals})=>\#{kindToString o}.\#{n.value}(\#{args})"#

export
conFFI : Kind -> Nat -> String
conFFI n k =
  let vs = take k argNames
      vals = fastConcat $ intersperse "," vs
   in foreignBrowser #"(\#{vals})=> new \#{kindToString n}(\#{vals})"#

export
conFFIVarArg : Kind -> Nat -> String
conFFIVarArg n k =
  let vs = take (pred k) argNames
      vals = fastConcat $ intersperse "," (vs ++ ["va"])
      args = fastConcat $ intersperse "," (vs ++ ["...va()"])
   in foreignBrowser #"(\#{vals})=> new \#{kindToString n}(\#{args})"#

export
dictConFFI : List ArgumentName -> String
dictConFFI ns =
  let vs     = take (length ns) argNames
      vals   = fastConcat $ intersperse "," vs
      fields = fastConcat $ intersperse "," (zipWith app vs ns)
   in foreignBrowser #"(\#{vals})=> {\#{fields}}"#

  where app : String -> ArgumentName -> String
        app v a = a.value ++ ": " ++ v

export
getterFFI : String
getterFFI = foreignBrowser "(o,x)=>o[x]"

export
setterFFI : String
setterFFI = foreignBrowser "(o,x,v)=>o[x] = v"

export
callbackFFI : Nat -> String
callbackFFI n =
  let vs = fastConcat $ intersperse "," $ take n argNames
   in foreignBrowser #"x=>(\#{vs})=>x(\#{vs})()"#


text:
module Education

public export
record Education where
  constructor CreateEducation
  university : Integer
  universityName : String
  faculty : Integer
  facultyName : String
  graduation : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
-- Idris2

module Sinter

import Data.List
import Data.Vect
import Data.String.Extra

import Core.Context
import Core.CompileExpr

import Compiler.LambdaLift
import Compiler.Common
import Idris.Driver

------------
-- SINTER --
------------

sqBrack : String -> String
sqBrack s = "[ " ++ s ++ " ]"

-- only literals in sinter are ints
data SinterLit
  = SinInt Int Nat    -- TODO: Int is value then width
  | SinStr String

-- IDs are basically strings (not really, TODO)
data SinterID = MkSinterID String

genSinterID : SinterID -> String
genSinterID (MkSinterID id_) = id_

Show SinterID where
  show = genSinterID

-- declared here, defined later
data SinterGlobal : Type where

-- an expression is a list of expressions, an ID, or a literal
data Sexpr : Type where
  SexprList : (es : List Sexpr) -> Sexpr
  SexprID : (id_ : SinterID) -> Sexpr
  SexprLit : SinterLit -> Sexpr
  SexprLet : (next : Sexpr) -> (defFun : SinterGlobal) -> Sexpr  -- let-in for sinter

genSexpr : Sexpr -> String
genSexpr (SexprList []) = "[]"

genSexpr (SexprList es) =
  let
    exprs = map genSexpr es
  in sqBrack $ join " " exprs
--  in "[ " ++ (concat exprs) ++ " ]"

genSexpr (SexprID id_) = show id_

genSexpr (SexprLit (SinInt v w)) =
  "( " ++ show w ++ "; " ++ show v ++ " )"

genSexpr (SexprLit (SinStr s)) =
  show s

-- TODO
genSexpr (SexprLet next defFun) =
  genSexpr next

Show Sexpr where
  show = genSexpr

-------------------------------
-- Things that can be global --
-------------------------------

-- declared earlier, defined here
data SinterGlobal = SinDef SinterID (List SinterID) Sexpr
                  | SinDecl SinterID (List SinterID)
                  | SinType SinterID (List SinterID)

genSinter : SinterGlobal -> String
genSinter (SinDef fName args body) =
  let
    args' = map show args
    argsStr = sqBrack $ join " " args'
  in sqBrack $ "def " ++ show fName ++ " " ++ argsStr ++ "\n\t"
                ++ genSexpr body

genSinter (SinDecl fName args) =
  let
    args' = map show args
    argsStr = sqBrack $ join " " args'
  in sqBrack $ "dec " ++ show fName ++ " " ++ argsStr

genSinter (SinType tName membs) =
  let
    membs' = map show membs
    membsStr = sqBrack $ join " " membs'
  in sqBrack $ "type " ++ show tName ++ membsStr

Show SinterGlobal where
  show = genSinter

testCase : SinterGlobal
testCase = SinDef (MkSinterID "test") [(MkSinterID "arg1"), (MkSinterID "arg2")]
                  (SexprList [SexprLit (SinInt 1 2)])

-----------------------
-- Sinter primitives --
-----------------------

||| Primitive implemented in sinter
sinterPrim : String -> Sexpr
sinterPrim name = SexprID $ MkSinterID name

||| Primitive supplied by stdlib
sinterStdlib : String -> Sexpr
sinterStdlib name = SexprID $ MkSinterID ("stdlib_" ++ name)

||| Call the special sinter function for creating closures
sinterClosureCon : Sexpr
sinterClosureCon = sinterPrim ">makeClosure"

||| Call the special sinter function for running or adding args to closures
sinterClosureAdd : Sexpr
sinterClosureAdd = sinterPrim ">closureAddElem"

||| Crash sinter very inelegantly
sinterCrash : Sexpr
sinterCrash = SexprList [ sinterPrim "CRASH" ]

------------------
-- GORY DETAILS --
------------------

||| Symbol for indicating membership of namespace: "--|"
specialSep : String
specialSep = "--|"

||| Symbol for indicating record access: "."
recordAcc : String
recordAcc = "."

||| Separate two ids by "specialSep"
stitch : SinterID -> SinterID -> SinterID
stitch (MkSinterID x) (MkSinterID y) = MkSinterID $ x ++ specialSep ++ y

||| Turn a NS into a string separated by "specialSep"
mangleNS : Namespace -> SinterID
mangleNS ns = MkSinterID $ showNSWithSep specialSep ns

||| Sinter doesn't have a concept of NameSpaces, so define unique, but
||| identifiable names/strings instead.
mangle : Name -> SinterID
mangle (NS nameSpace name) =
  let
    nameSpace' = mangleNS nameSpace
    name' = mangle name
  in
    stitch nameSpace' name'

mangle (UN x) = MkSinterID x

mangle (MN x i) = MkSinterID $ x ++ "-" ++ show i

mangle (PV n i) = MkSinterID $ (show $ mangle n) ++ "-" ++ show i

--mangle (DN x y) = MkSinterID x      -- FIXME: correct? (assumes x repr.s y)
mangle (DN _ y) = mangle y            -- ^ incorrect! the Name itself still
                                      -- needs to be mangled; the way to display
                                      -- it doesn't necessarily match our way of
                                      -- representing names.

mangle (RF x) = MkSinterID $ recordAcc ++ x

mangle (Nested (i, j) n) =
  MkSinterID $ "nested_" ++ (show i) ++ "_" ++ (show j) ++ (show $ mangle n)

-- string repr.n of case followed by unique Int (?)
mangle (CaseBlock x i) = MkSinterID $ "case_" ++ x ++ "-" ++ (show i)

mangle (WithBlock x i) = MkSinterID $ "with_" ++ x ++ "-" ++ (show i)

mangle (Resolved i) = MkSinterID $ "resolved_" ++ (show i)

idrisWorld : Sexpr
idrisWorld = SexprID $ MkSinterID "**IDRIS_WORLD**"

||| Assume < 2^31 number of args to any function (seriously, what would you do
||| with 2^31 args?...)
nArgsWidth : Nat
nArgsWidth = 32

||| Turn all the arguments (including the scope) into SinterIDs
superArgsToSinter : List Name -> List SinterID
superArgsToSinter ns = map mangle ns

-- Constants

constantToSexpr : Constant -> Sexpr
constantToSexpr (I x) = SexprLit $ SinInt (cast x) 64
constantToSexpr (BI x) = ?sexprConstBI
constantToSexpr (B8 x) = SexprLit $ SinInt (cast x) 8
constantToSexpr (B16 x) = SexprLit $ SinInt (cast x) 16
constantToSexpr (B32 x) = SexprLit $ SinInt (cast x) 32
constantToSexpr (B64 x) = SexprLit $ SinInt (cast x) 64
constantToSexpr (Str x) = SexprLit $ SinStr x
constantToSexpr (Ch x) = ?constantToSexpr_rhs_8
constantToSexpr (Db x) = ?constantToSexpr_rhs_9
constantToSexpr WorldVal = idrisWorld
constantToSexpr IntType = ?constantToSexpr_rhs_11
constantToSexpr IntegerType = ?constantToSexpr_rhs_12
constantToSexpr Bits8Type = ?constantToSexpr_rhs_13
constantToSexpr Bits16Type = ?constantToSexpr_rhs_14
constantToSexpr Bits32Type = ?constantToSexpr_rhs_15
constantToSexpr Bits64Type = ?constantToSexpr_rhs_16
constantToSexpr StringType = ?constantToSexpr_rhs_17
constantToSexpr CharType = ?constantToSexpr_rhs_18
constantToSexpr DoubleType = ?constantToSexpr_rhs_19
constantToSexpr WorldType = ?constantToSexpr_rhs_20

mutual
  -- Primitive Functions

  primFnToSexpr : {scope : _} -> {args : _}
                -> PrimFn arity -> Vect arity (Lifted (scope ++ args)) -> Sexpr
  primFnToSexpr (Add ty) [x, y] =
    SexprList [ sinterStdlib "add", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (Sub ty) [x, y] =
    SexprList [ sinterStdlib "sub", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (Mul ty) [x, y] =
    SexprList [ sinterStdlib "mul", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (Div ty) [x, y] =
    SexprList [ sinterStdlib "div", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (Mod ty) [x, y] =
    SexprList [ sinterStdlib "mod", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (Neg ty) [x] =
    SexprList [ sinterStdlib "neg", liftedToSexpr x ]

  primFnToSexpr (ShiftL ty) [x, y] =
    SexprList [ sinterStdlib "shiftl", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (ShiftR ty) [x, y] =
    SexprList [ sinterStdlib "shiftr", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (BAnd ty) [x, y] =
    SexprList [ sinterStdlib "bitwAnd", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (BOr ty) [x, y] =
    SexprList [ sinterStdlib "bitwOr", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (BXOr ty) [x, y] =
    SexprList [ sinterStdlib "bitwXor", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (LT ty) [x, y] =
    SexprList [ sinterStdlib "lt", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (LTE ty) [x, y] =
    SexprList [ sinterStdlib "lte", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (EQ ty) [x, y] =
    SexprList [ sinterStdlib "eq", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (GTE ty) [x, y] =
    SexprList [ sinterStdlib "gte", liftedToSexpr x, liftedToSexpr y ]

  primFnToSexpr (GT ty) [x, y] =
    SexprList [ sinterStdlib "gt", liftedToSexpr x, liftedToSexpr y ]

  -- TODO
  primFnToSexpr StrLength [s] = ?sinterStrLen
  primFnToSexpr StrHead [s] = ?sinterStrHead
  primFnToSexpr StrTail [s] = ?sinterStrTail
  primFnToSexpr StrIndex [s, i] = ?sinterStrIndex
  primFnToSexpr StrCons [s1, s2] = ?sinterStrCons
  primFnToSexpr StrAppend [s1, s2] =
    SexprList [ sinterStdlib "strAppend", liftedToSexpr s1, liftedToSexpr s2 ]
  primFnToSexpr StrReverse [s] = ?sinterStrReverse
  primFnToSexpr StrSubstr [i, j, s] = ?sinterSubstr

  -- TODO
  primFnToSexpr DoubleExp [d] = ?primFnToSexpr_rhs_25
  primFnToSexpr DoubleLog [d] = ?primFnToSexpr_rhs_26
  primFnToSexpr DoubleSin [d] = ?primFnToSexpr_rhs_27
  primFnToSexpr DoubleCos [d] = ?primFnToSexpr_rhs_28
  primFnToSexpr DoubleTan [d] = ?primFnToSexpr_rhs_29
  primFnToSexpr DoubleASin [d] = ?primFnToSexpr_rhs_30
  primFnToSexpr DoubleACos [d] = ?primFnToSexpr_rhs_31
  primFnToSexpr DoubleATan [d] = ?primFnToSexpr_rhs_32
  primFnToSexpr DoubleSqrt [d] = ?primFnToSexpr_rhs_33
  primFnToSexpr DoubleFloor [d] = ?primFnToSexpr_rhs_34
  primFnToSexpr DoubleCeiling [d] = ?primFnToSexpr_rhs_35

  -- TODO
  primFnToSexpr (Cast x y) [z] = ?primFnToSexpr_rhs_36
  primFnToSexpr BelieveMe [_, _, thing] = liftedToSexpr thing
                                        -- ^ I believe this is correct?

  primFnToSexpr Crash [fc, reason] =
    sinterCrash

  ||| Create a call to a function which evaluates `in` over `let`
  |||   let f x = y in z
  ||| is equivalent to
  |||   (\f . z) (\x . y)
  lletToSexpr : {scope : _} -> {args : _}
              -> FC
              -> (n : Name)
              -> (existing : Lifted (scope ++ args))
              -> (in_expr : Lifted (n :: (scope ++ args)))
              -> Sexpr
  lletToSexpr fc n existing in_expr =
    let
      -- containing IN
      vars = scope ++ args
      cursedFuncName = show fc ++ show n
      cFunName = MkSinterID cursedFuncName
      cFunArgs = (mangle n) :: map mangle vars
      cFunBody = liftedToSexpr {scope=(n :: scope)} {args=args} in_expr
      cFunDef = SinDef cFunName cFunArgs cFunBody

      -- applying this
      cFunCallArgs = liftedToSexpr {scope=scope} {args=args} existing
      cFunCall = SexprList $ (SexprID cFunName)
                             :: cFunCallArgs
                             :: (map (SexprID . mangle) vars)
    in
      SexprLet cFunCall cFunDef

  -- Functions

  ||| Compile the definition to sexprs
  liftedToSexpr : {scope : _} -> {args : _} -> Lifted (scope ++ args) -> Sexpr
  -- idx points to right variable; de bruijn index
  liftedToSexpr (LLocal {idx} fc p) = -- ?llocalToSinter
    case take (S idx) (scope ++ args) of
         -- FIXME: this is very naughty and should be handled better
         [] => assert_total $ idris_crash "scope ++ args did not contain name"
         (n :: _) => SexprID $ mangle n

  -- complete function call
  liftedToSexpr (LAppName fc _ n fArgs) =
    let
      funName = SexprID $ mangle n
      funArgs = map (liftedToSexpr {scope=scope} {args=args}) fArgs
    in
      SexprList $ funName :: funArgs

  -- partial function call
  liftedToSexpr (LUnderApp fc n missing fArgs) =
    let
      sinName  = SexprID $ mangle n
      sinMiss  = SexprLit $ SinInt (cast missing) nArgsWidth
      nArgs    = length args
      sinNArgs = SexprLit $ SinInt (cast nArgs) nArgsWidth
      -- number of args function expects
      sinArity = SexprLit $ SinInt (cast (missing + nArgs)) nArgsWidth
      -- list of arguments
      --sinArgs  = SexprList $ map liftedToSexpr fArgs
      sinArgs  = SexprList $ map (liftedToSexpr {scope=scope} {args=args}) fArgs
    in
      -- make a closure containing the above info (sinter-specific closure)
      SexprList [sinterClosureCon , sinName , sinArity , sinNArgs , sinArgs]

  -- application of a closure to another argument; potentially to the last arg
  liftedToSexpr (LApp fc _ closure arg) =
    let
      sinClosure = liftedToSexpr closure
      sinArg = liftedToSexpr arg
    in
      SexprList [sinterClosureAdd, sinClosure, sinArg]

  -- let expressions
  liftedToSexpr (LLet fc n existing in_expr) =
    lletToSexpr fc n existing in_expr

  -- constructor calls
  liftedToSexpr (LCon fc n tag xs) =
    let
      (MkSinterID mn) = mangle n
      name = MkSinterID $ mn ++ show tag
      fArgs = map (liftedToSexpr {scope=scope} {args=args}) xs
    in
      SexprList $ (SexprID name) :: fArgs

  -- primitive operators
  liftedToSexpr (LOp fc _ x xs) =
    primFnToSexpr x xs

  liftedToSexpr (LExtPrim fc _ p xs) = ?liftedToSexpr_rhs_8

  liftedToSexpr (LConCase fc x xs y) = ?liftedToSexpr_rhs_9

  liftedToSexpr (LConstCase fc lvars lConAlts m_default) =
    let
      comparator = liftedToSexpr lvars
    in
      case m_default of
           Nothing => sinterCrash
           (Just x) => ifHelper comparator lConAlts (liftedToSexpr x)

  liftedToSexpr (LPrimVal fc x) = constantToSexpr x

  liftedToSexpr (LErased fc) =
    SexprLit $ SinInt 0 0

  liftedToSexpr (LCrash fc x) =
    sinterCrash

  ifHelper : {scope : _} -> {args : _}
           -> Sexpr -> List (LiftedConstAlt (scope ++ args)) -> Sexpr -> Sexpr
  ifHelper x [] def = def
  ifHelper x ((MkLConstAlt c body) :: alts) def =
    let
      sinC = constantToSexpr c
      sinBody = liftedToSexpr body
      ifCond = SexprList [ (sinterStdlib "eq") , x , sinC ]
      elseBody = ifHelper x alts def
    in
      SexprList [ SexprID $ MkSinterID "if" , ifCond, sinBody , elseBody ,
                  SexprID $ MkSinterID "32" ]

||| Compile a constructor's definition
liftedConToSinter : (tag : Maybe Int)
                  -> (arity : Nat)
                  -> (nt : Maybe Nat)
                  -> Core SinterGlobal
liftedConToSinter tag arity nt = ?liftedConToSinter_rhs

||| Compile a pair of Name and its associated definition into a SinterGlobal,
||| i.e.:
|||   - mangle the Name into a valid sinter name
|||   - compile the definition into a sexpr
liftedToSinter : (Name, LiftedDef) -> Core SinterGlobal

-- FUNCTIONS
liftedToSinter (name, (MkLFun args scope body)) =
  let
    sinName = mangle name
    superArgs = args ++ reverse scope
    sinArgs = superArgsToSinter superArgs
    sinDefn = liftedToSexpr body
  in
    pure $ SinDef sinName sinArgs sinDefn

-- CONSTRUCTORS
liftedToSinter (name, (MkLCon tag arity nt)) =
  let
    sinName = mangle name
    sinDefn = liftedConToSinter tag arity nt
  in
    pure $ SinType sinName ?liftedConBody

-- FFI CALLS
liftedToSinter (name, (MkLForeign ccs fargs x)) = ?liftedFFICalltoSinter

-- GLOBAL ERRORS
liftedToSinter (name, (MkLError x)) = ?liftedErrorToSinter

----------------
-- TOP OF API --
----------------

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
        ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile context tmpDir outputDir term outfile =
  do compData <- getCompileData False Lifted term
     let defs = lambdaLifted compData
     sinterGlobs <- traverse liftedToSinter defs
     -- readyForCG <- traverse bubbleLets sinterGlobs
     ?compile_rhs

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute context tmpDir term =
  throw $ InternalError "Sinter backend can only compile, sorry."

sinterCodegen : Codegen
sinterCodegen = MkCG compile execute

main : IO ()
main = mainWithCodegens [("sinter", sinterCodegen)]


text:
module Main

import System
import System.Concurrency.Raw

recvMsg : IO (Ptr, String)
recvMsg = getMsg

pong : IO ()
pong = do (sender, x) <- recvMsg
          putStrLn x
          putStrLn "Received"
          sendToThread sender 0 "Hello to you too!"
          pure ()

ping : Ptr -> IO ()
ping thread = do me <- getMyVM
                 sendToThread thread 0 (me, "Hello!")
                 pure ()

pingpong : IO ()
pingpong
     = do th <- fork pong
          putStrLn "Sending"
          ping th
          reply <- getMsg
          putStrLn reply
          usleep 100000
          putStrLn "Finished"

main : IO ()
main = do pingpong; pingpong; pingpong

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
import Mod

main : IO ()
main = printLn (fn (100 * 100))


text:
module Math.Algebra.Quantum.Qubit

import public Data.Fin
import public Data.Vect
import public Data.Matrix
import public Data.Matrix.Algebraic
--import public Data.Matrix.Numeric
import public Data.Complex

import public Control.Algebra
import public Control.Algebra.VectorSpace

%access public export
%default total

C : Type
C = Complex Double

-- Euler
e : Double
e = exp 1

-- Imaginary unit
i : C
i = 0:+1

-- Complex Pi
pii : C
pii = pi:+0

-- Complex exponentiation
expi : C -> C
expi z =
  let es = exp $ realPart z in
    es * (cos $ imagPart z) :+ es * (sin $ imagPart z)

-- WIP
-- really to enforce conjugate transpose we need to have a 1-col matrix
-- and a 1-row matrix as a Bra i.e.
-- Ket = Matrix 2 1 C
-- Bra = Matrix 1 2 C
-- them implement all the Semigroup/Monoid/Group/InnerProductSpace etc. instances for these
-- along with interfaces for (ant general matrix classes, definite, normal, semi-definite etc.?)
-- Operator = Matrix 2 2 C
-- Unitary : Operator where ...
-- Hermitian : Unitary where ...

-- in some sense a vector is a linear transformation anyway especially when
-- you consider dot product as linear transformation to 1-d field
-- hermitian = dagger = adjoint

mmap : (a -> a) -> Matrix n m a -> Matrix n m a
mmap = map . map

-- TODO instead of aliases we should define new types and classes

Ket : Type
Ket = Matrix 2 1 C

Bra: Type
Bra = Matrix 1 2 C

ket : C -> C -> Ket
ket a b = [[a], [b]]

bra : C -> C -> Bra
bra a b = [[a, b]]

qubit : C -> C -> Ket
qubit = ket

one : Ket
one = qubit (0:+0) (1:+0)

zero : Ket
zero = qubit (1:+0) (0:+0)

bra2ket : Bra -> Ket
bra2ket b = Data.Vect.transpose $ mmap conjugate b

ket2bra : Ket -> Bra
ket2bra k = Data.Vect.transpose $ mmap conjugate k

--

Operator : Type
Operator = Matrix 2 2 C

Id : Operator
Id = [[1:+0, 0:+0], [0:+0, 1:+0]]

{-
Data.Matrix.Agebraic now takes care of these implementations

[AddComplexSemigroup] Semigroup C where
  (<+>) z w = z + w

[MulComplexSemigroup] Semigroup C where
  (<+>) z w = z * w

[AddComplexMonoid] Monoid C using AddComplexSemigroup where
  neutral = 0:+0

[MulComplexMonoid] Monoid C using MulComplexSemigroup where
  neutral = 1:+0

Group C using MulComplexMonoid where
  inverse z = 1 / z

AbelianGroup C where { }

Ring C where
  (<.>) z w = z * w

RingWithUnity C where
  unity = 1:+0

-- Kets upto InnerProductSpace

Semigroup Ket where
  (<+>) u v = zipWith (+) u v

Monoid Ket where
  neutral = [0:+0, 0:+0]

Group Ket where
  inverse u = map (1 /) u

AbelianGroup Ket where { }

Module C Ket where
  (<#>) c v = map (* c) v

-}

{-
InnerProductSpace C Ket where
  (<||>) u v = sum $ zipWith (*) u v

test : C
test = one <||> one
-}

-- Local Variables:
-- idris-load-packages: ("base" "contrib")
-- End:

max_stars_repo_name: sebeaumont/hilbert

max_issues_repo_name: sebeaumont/hilbert

max_forks_repo_name: sebeaumont/hilbert


text:
module Main

data Identity a = Id a

runIdentity : Identity a -> a
runIdentity (Id a) = a

instance Functor Identity where
  map f (Id x) = Id (f x)

instance Applicative Identity where
  pure = Id
  (Id f) <$> (Id x) = Id (f x)

instance Monad Identity where
  (Id m) >>= f = f m

data Source : {r : Type} -> (m : Type -> Type) -> (a : Type) -> Type where
  Src : (r -> (r -> a -> m r) -> m r) -> Source {r} m a

runSource : {r : Type} -> Source {r} m a -> r -> (r -> a -> m r) -> m r
runSource (Src await) = await

Conduit : {r : Type} -> Type -> (Type -> Type) -> Type -> Type
Conduit {r} a m b = Source {r} m a -> Source {r} m b

Sink : {r : Type} -> Type -> (Type -> Type) -> Type -> Type
Sink {r} a m s = Source {r} m a -> m s

instance Functor (Source {r} m) where
    map f (Src await) = Src $ \z, yield => await z (\r => yield r . f)

foldM : Monad m => (r -> a -> m r) -> r -> List a -> m r
foldM f z []        = return z
foldM f z (x :: xs) = f z x >>= flip (foldM f) xs

source : {r : Type} -> (r -> (r -> a -> m r) -> m r) -> Source {r} m a
source = Src

sourceList : Monad m => List a -> Source m a
sourceList xs = source $ \z, yield => foldM yield z xs

mapC : Monad m => {r : Type} -> (a -> b) -> Conduit {r} a m b
mapC = map

sinkList : Monad m => Sink {r = List a} a m (List a)
sinkList (Src await) = await Prelude.List.Nil (\xs, x => return (x :: xs))

main : IO ()
main = print $ runIdentity $ sinkList $ mapC (+1) $ sourceList [1..10]

max_stars_repo_name: jwiegley/simple-conduit

max_issues_repo_name: jwiegley/simple-conduit

max_forks_repo_name: jwiegley/simple-conduit


text:
module Data.GIS

import Control.Algebra
import Control.Algebra.NumericImplementations
import Data.Int.Algebra
import Data.Music

%access public export

interface Group ivls => GIS space ivls | space where
  ref     : space
  int     : space -> space -> ivls
  LABEL   : space -> ivls

  int s t = LABEL t <-> LABEL s
  -- LABEL s = if s == ref then neutral else int ref s

[IntScalarGIS] GIS Int Int where
  ref   = 0
  LABEL = id

[DiatonicPitchGIS] GIS Diatonic.Pitch Int where
  ref   = (C, 0)
  LABEL = cast

[PSpaceGIS] GIS Chromatic.Pitch Int where
  ref   = (C, 0)
  LABEL = cast

[PCSpaceGIS] GIS Chromatic.PitchClass (Zn 12) where
  ref   = C
  LABEL = cast

[DiatonicPitchClassGIS] GIS Diatonic.PitchClass (Zn 7) where
  ref   = C
  LABEL = cast

[PitchClassRefFGIS] GIS Chromatic.PitchClass (Zn 12) where
  ref     = F
  LABEL s = MkZn (cast s) <-> MkZn 5

max_stars_repo_name: yurrriq/gis

max_issues_repo_name: yurrriq/gis

max_forks_repo_name: yurrriq/gis


text:
module Props.String

import Props.Util

%access public export

NonEmpty : String -> Type
NonEmpty s = Denied (decEq "" s)

max_stars_repo_name: janschultecom/idris-refined

max_issues_repo_name: janschultecom/idris-refined

max_forks_repo_name: janschultecom/idris-refined


text:
module Main

f : Int -> Bool
f n = if n `mod` 2 == 0 then True else False

factx : Int -> Lazy Int
factx 0 = 0
factx n = n + factx (n - 1) + sx n
        where
            sx 1 = 3
            sx n = 1 + sx (n - 1)

main : IO ()
main = do
    let t = sum [0,50,50]
    -- let t = 100
    putStrLn $ show $ t
    let abc = factx $ t
    putStrLn $ show $ Force abc
    -- putStrLn $ show $ abc
    putStrLn $ show $ f abc

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module GRIN.Analysis.Effects

import Data.List
import Data.List1
import Data.SortedMap as Map

import GRIN.AST
import GRIN.GrinState

filter : (a -> Bool) -> List1 a -> List a
filter pred = filter pred . forget

data PartialResult : Type -> Type where
    Cond : List1 name -> PartialResult name
    Definite : Effectful -> PartialResult name

Semigroup (PartialResult name) where
    Cond xs <+> Cond ys = Cond $ xs ++ ys
    Definite NoEffect <+> e = e
    Definite Effect <+> e = Definite Effect
    e <+> Definite NoEffect = e
    e <+> Definite Effect = Definite Effect

Monoid (PartialResult name) where
    neutral = Definite NoEffect

parameters {auto _ : Eq name} (env : SortedMap name (PartialResult name)) (current : name)
  mutual
    effectSExp : SExp name -> PartialResult name
    effectSExp (Do x) = effectExp x
    effectSExp (App x xs) = case lookup x env of
        Nothing => Cond (singleton x)
        Just (Cond xs) => case filter (/= current) xs of
            [] => Definite NoEffect
            (x :: xs) => Cond $ x ::: xs
        Just eff@(Definite _) => eff
    effectSExp (Pure x) = Definite NoEffect
    effectSExp (Store x) = Definite NoEffect
    effectSExp (Fetch x y) = Definite NoEffect
    effectSExp (FetchI x k y) = Definite NoEffect
    effectSExp (Update x y) = Definite Effect

    effectExp : Exp name -> PartialResult name
    effectExp (SimpleExp e) = effectSExp e
    effectExp (Bind _ rhs rest) = effectSExp rhs <+> effectExp rest
    effectExp (Case _ alts) = foldMap effectAlt alts

    effectAlt : Alt name -> PartialResult name
    effectAlt (MkAlt _ exp) = effectExp exp

effectDef : Eq name => SortedMap name (PartialResult name) -> Def name -> PartialResult name
effectDef env def = effectExp env def.defName def.body

addExternToEnv : SortedMap name (PartialResult name) -> Extern name -> SortedMap name (PartialResult name)
addExternToEnv env ext = insert ext.extName (Definite ext.eff) env

addDefToEnv : Eq name => SortedMap name (PartialResult name) -> Def name -> SortedMap name (PartialResult name)
addDefToEnv env def = insert def.defName (effectDef env def) env


text:
import Data.IOArray

import System

main : IO ()
main
    = do x <- newArray 20
         True <- writeArray x 10 "Hello"
           | False => do putStrLn "should success 1"
                         exitFailure
         True <- writeArray x 11 "World"
           | False => do putStrLn "should success 2"
                         exitFailure

         False <- writeArray x 20 "World"
           | True => do putStrLn "should fail"
                        exitFailure

         printLn !(toList x)

         y <- fromList (map Just [1,2,3,4,5])
         printLn !(toList y)


text:
module Libraries.Text.Lexer.Tokenizer

import Data.List
import Data.Either
import Data.Nat
import Data.String

import Libraries.Data.String.Extra
import Libraries.Text.Lexer.Core
import Libraries.Text.Lexer
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util

import public Libraries.Control.Delayed
import public Libraries.Text.Bounded

%default total

||| Description of a language's tokenization rule.
export
data Tokenizer : (tokenType : Type) -> Type where
     Match : Lexer -> (String -> tokenType) -> Tokenizer tokenType
     Compose : (begin : Lexer) ->
               (mapBegin : String -> tokenType) ->
               (tagger : String -> tag) ->
               (middle : Inf (tag -> Tokenizer tokenType)) ->
               (end : tag -> Lexer) ->
               (mapEnd : String -> tokenType) ->
               Tokenizer tokenType
     Alt : Tokenizer tokenType -> Lazy (Tokenizer tokenType) -> Tokenizer tokenType

||| Alternative tokenizer rules.
export
(<|>) : Tokenizer t -> Lazy (Tokenizer t) -> Tokenizer t
(<|>) = Alt

||| Match on a recogniser and cast the string to a token.
export
match : Lexer -> (String -> a) -> Tokenizer a
match = Match

||| Compose other tokenizer. Language composition should be quoted between
||| a begin lexer and a end lexer. The begin token can be used to generate
||| the composition tokenizer and the end lexer.
export
compose : (begin : Lexer) ->
          (mapBegin : String -> a) ->
          (tagger : String -> tag) ->
          (middle : Inf (tag -> Tokenizer a)) ->
          (end : tag -> Lexer) ->
          (mapEnd : String -> a) ->
          Tokenizer a
compose = Compose

||| Stop reason why tokenizer can't make more progress.
||| @ ComposeNotClosing carries the span of composition begin token in the
|||                     form of `(startLine, startCol), (endLine, endCol)`.
public export
data StopReason = EndInput | NoRuleApply | ComposeNotClosing (Int, Int) (Int, Int)

export
Show StopReason where
  show EndInput = "EndInput"
  show NoRuleApply = "NoRuleApply"
  show (ComposeNotClosing start end) = "ComposeNotClosing " ++ show start ++ " " ++ show end

export
Pretty StopReason where
  pretty EndInput = pretty "EndInput"
  pretty NoRuleApply = pretty "NoRuleApply"
  pretty (ComposeNotClosing start end) = "ComposeNotClosing" <++> pretty start <++> pretty end

tokenise : Lexer ->
           Tokenizer a ->
           (line, col : Int) -> List (WithBounds a) ->
           List Char ->
           (List (WithBounds a), (StopReason, Int, Int, List Char))
tokenise reject tokenizer line col acc [] = (reverse acc, EndInput, (line, col, []))
tokenise reject tokenizer line col acc str
    = case scan reject [] str of
           Just _ => (reverse acc, (EndInput, line, col, str))
           Nothing => case getFirstMatch tokenizer str of
                           Right (toks, line', col', rest) =>
                               -- assert total because getFirstMatch must consume something
                               assert_total (tokenise reject tokenizer line' col' (toks ++ acc) rest)
                           Left reason => (reverse acc, reason, (line, col, str))
  where
    countNLs : List Char -> Nat
    countNLs str = List.length (filter (== '\n') str)

    getCols : List Char -> Int -> Int
    getCols x c
        = case span (/= '\n') x of
               (incol, []) => c + cast (length incol)
               (incol, _) => cast (length incol)

    -- get the next lexeme using the `Lexer` in argument, its position and the input
    -- Returns the new position, the lexeme parsed and the rest of the input
    -- If parsing the lexer fails, this returns `Nothing`
    getNext : (lexer : Lexer) ->  (line, col : Int) -> (input : List Char) -> Maybe (String, Int, Int, List Char)
    getNext lexer line col str =
      let Just (token, rest) = scan lexer [] str
            | _ => Nothing
          line' = line + cast (countNLs token)
          col' = getCols token col
          tokenStr = fastPack $ reverse token
       in pure (tokenStr, line', col', rest)

    getFirstMatch : Tokenizer a -> List Char ->
                    Either StopReason (List (WithBounds a), Int, Int, List Char)
    getFirstMatch (Match lex fn) str
        = let Just (tok, line', col', rest) = getNext lex line col str
                | _ => Left NoRuleApply
              tok' = MkBounded (fn tok) False (MkBounds line col line' col')
           in Right ([tok'], line', col', rest)
    getFirstMatch (Compose begin mapBegin tagger middleFn endFn mapEnd) str
        = let Just (beginTok', line', col' , rest) = getNext begin line col str
                | Nothing => Left NoRuleApply
              tag = tagger beginTok'
              middle = middleFn tag
              end = endFn tag
              beginTok'' = MkBounded (mapBegin beginTok') False (MkBounds line col line' col')
              (midToks, (reason, line'', col'', rest'')) =
                    assert_total $ tokenise end middle line' col' [] rest
           in case reason of
                   (ComposeNotClosing _ _) => Left reason
                   _ => let Just (endTok', lineEnd, colEnd, restEnd) =
                                getNext end line'' col'' rest''
                              | _ => Left $ ComposeNotClosing (line, col) (line', col')
                            endTok'' = MkBounded (mapEnd endTok') False (MkBounds line'' col'' lineEnd colEnd)
                         in Right ([endTok''] ++ reverse midToks ++ [beginTok''], lineEnd, colEnd, restEnd)
    getFirstMatch (Alt t1 t2) str
        = case getFirstMatch t1 str of
               Right result => Right result
               Left reason@(ComposeNotClosing _ _) => Left reason
               Left _ => getFirstMatch t2 str

export
lexTo : Lexer ->
        Tokenizer a ->
        String ->
        (List (WithBounds a), (StopReason, Int, Int, String))
lexTo reject tokenizer str
    = let (ts, reason, (l, c, str')) =
              tokenise reject tokenizer 0 0 [] (fastUnpack str) in
          (ts, reason, (l, c, fastPack str'))

||| Given a tokenizer and an input string, return a list of recognised tokens,
||| and the line, column, and remainder of the input at the first point in the string
||| where there are no recognised tokens.
export
lex : Tokenizer a -> String -> (List (WithBounds a), (StopReason, Int, Int, String))
lex tokenizer str = lexTo (pred $ const False) tokenizer str


text:
module TTImp.Elab.Prim

import Core.TT

%default covering

export
checkPrim : FC -> Constant -> (Term vars, Term vars)
checkPrim fc (I i) = (PrimVal fc (I i), PrimVal fc IntType)
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 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)


text:
module Postgres.Data.PostgresType

import Data.List

%default total

-- see src/include/catalog/pg_type.h

--
-- Oid
--

||| Postgres Oids are just integers that have special
||| internal semantics within Postgres.
public export
data Oid : Type where
  MkOid : Int -> Oid

Eq Oid where
  (MkOid x) == (MkOid y) = x == y

Show Oid where
  show (MkOid oid) = show oid

||| Get an integer representation of an Oid. Probably only useful
||| when actually sending the Oid to Postgres for some reason.
export
oidToInt : Oid -> Int
oidToInt (MkOid x) = x

--
-- Type
--

||| Not an exhaustive list of types, just a short list of
||| builtins with explicit support in this library.
public export
data PType = PInteger
           | PDouble
           | PChar
           | PBoolean
           | PDate
           | PTime
           | PDatetime
           | PString
           | PJson
           | PUuid
           | POid
           | PArray PType
           | POther String
           | PUnknown Oid

export
Show PType where
  show PInteger   = "Integer"
  show PDouble    = "Double"
  show PChar      = "Char"
  show PBoolean   = "Boolean"
  show PDate      = "Date"
  show PTime      = "Time"
  show PDatetime  = "DateTime"
  show PString    = "String"
  show PJson      = "JSON"
  show PUuid      = "UUID"
  show POid       = "OID"
  show (PArray t) = (show t) ++ "[]"
  show (POther x) = "?" ++ x
  show (PUnknown (MkOid oid)) = "Oid: " ++ (show oid)

public export
data PColType : PType -> Type where
  MkColType : (nullable: Bool) -> (pt : PType) -> PColType pt

export
Show (PColType t) where
  show (MkColType _ x) = show x

public export
pType : PColType t -> PType
pType (MkColType _ t) = t

public export
nullable : PColType t -> Bool
nullable (MkColType n _) = n

--
-- Format Code
--

public export
data FormatCode = Text | Binary

export
Show FormatCode where
  show Text   = "Text"
  show Binary = "Binary"

--
-- Type Dictionary
--

export
data TypeDictionary : Type where
  MkTypeDictionary : List (Oid, PType) -> TypeDictionary

-- The dot accessor makes it like a record type where the
-- following accessor is public but the constructor is not.
||| A sorted list of type tuples (pairs of Oid and type).
||| Sorted by Oid.
export
(.types) : TypeDictionary -> List (Oid, PType)
(.types) (MkTypeDictionary xs) = xs

||| A sorted list of type tuples (pairs of Oid and type).
||| Sorted by Oid.
export
types : TypeDictionary -> List (Oid, PType)
types (MkTypeDictionary xs) = xs

export
empty : TypeDictionary
empty = MkTypeDictionary []

||| Create a dictionary of Postgres types. The dictionary is
||| sorted by Oid for future lookup.
export
typeDictionary : List (Oid, PType) -> TypeDictionary
typeDictionary xs = MkTypeDictionary (sortBy (compare `on` oidToInt . fst) xs)

||| Find the Postgres Type the given Oid refers to, or
||| admit defeat via PUnknown.
export
lookup : Oid -> TypeDictionary -> PType
lookup oid = maybe (PUnknown oid) id . lookup oid . types

export
Show TypeDictionary where
  show = concat . intersperse "\n" . map showTuple . types
    where
      showTuple : (Oid, PType) -> String
      showTuple (oid, type) = (show oid) ++ ": " ++ (show type)

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
||| Default configurations for the LSP server implementation capabilities.
|||
||| (C) The Idris Community, 2021
module Server.Capabilities

import Core.Metadata

import Language.JSON
import Language.LSP.Message

%default total

decor : List Decoration
decor = [Typ, Function, Data, Bound, Keyword, Namespace, Postulate, Module, Comment]

encodeDecorAsString : Decoration -> String
encodeDecorAsString Typ       = "type"        -- Type constructors
encodeDecorAsString Function  = "function"    -- Functions
encodeDecorAsString Data      = "enumMember"  -- Data constructors
encodeDecorAsString Bound     = "variable"    -- Bound variables
encodeDecorAsString Keyword   = "keyword"     -- Keywords
encodeDecorAsString Namespace = "namespace"   -- Explicit namespaces
encodeDecorAsString Postulate = "postulate"   -- Postulates (assert_total, believe_me, ...)
encodeDecorAsString Module    = "module"      -- Explicit module names
encodeDecorAsString Comment   = "comment"     -- Comments

||| Convert Decoration to legend index
export
encodeDecorAsNum : Decoration -> Int
encodeDecorAsNum Typ       = 0
encodeDecorAsNum Function  = 1
encodeDecorAsNum Data      = 2
encodeDecorAsNum Bound     = 3
encodeDecorAsNum Keyword   = 4
encodeDecorAsNum Namespace = 5
encodeDecorAsNum Postulate = 6
encodeDecorAsNum Module    = 7
encodeDecorAsNum Comment   = 8

syncOptions = MkTextDocumentSyncOptions
  { openClose         = Just True
  , change            = Just Incremental
  , willSave          = Nothing
  , willSaveWaitUntil = Nothing
  , save              = Just $ make $ MkSaveOptions (Just True)
  }

semanticTokensLegend = MkSemanticTokensLegend
  { tokenTypes = map encodeDecorAsString decor
  , tokenModifiers = []
  }

semanticTokensOptions = MkSemanticTokensOptions
  { legend = semanticTokensLegend
  , range = Just $ make False
  , full = Just $ make True
  }

completionOptions = MkCompletionOptions
  { workDoneProgress    = Nothing
  , triggerCharacters   = Just []
  , allCommitCharacters = Just []
  , resolveProvider     = Nothing
  }

signatureHelpOptions = MkSignatureHelpOptions
  { workDoneProgress    = Nothing
  , triggerCharacters   = Nothing
  , retriggerCharacters = Nothing
  }

definitionOptions = MkDefinitionOptions
  { workDoneProgress = Just False
  }

documentSymbolOptions = MkDocumentSymbolOptions
  { workDoneProgress = Nothing
  , label            = Nothing
  }

codeActionOptions = MkCodeActionOptions
  { workDoneProgress = Nothing
  , codeActionKinds  = Nothing
  , resolveProvider  = Just False
  }

codeLensOptions = MkCodeLensOptions
  { workDoneProgress = Nothing
  , resolveProvider  = Nothing
  }

documentLinkOptions = MkDocumentLinkOptions
  { workDoneProgress = Nothing
  , resolveProvider  = Nothing
  }

executeCommandOptions = MkExecuteCommandOptions
  { workDoneProgress = Nothing
  , commands         = ["repl", "exprSearchWithHints", "refineHoleWithHints", "metavars"]
  }

workspaceFoldersServerCapabilities = MkWorkspaceFoldersServerCapabilities
  { supported           = Just False
  , changeNotifications = Nothing
  }

fileOperationServerCapabilities = MkFileOperationsServerCapabilities
  { didCreate  = Nothing
  , willCreate = Nothing
  , didRename  = Nothing
  , willRename = Nothing
  , didDelete  = Nothing
  , willDelete = Nothing
  }

workspaceServerCapabilities = MkWorkspaceServerCapabilities
  { workspaceFolders = Just workspaceFoldersServerCapabilities
  , fileOperations   = Just fileOperationServerCapabilities
  }

||| Default server capabilities to be sent to clients during the initialization protocol.
export
serverCapabilities : ServerCapabilities
serverCapabilities = MkServerCapabilities
  { textDocumentSync                 = Just $ make syncOptions
  , completionProvider               = Just completionOptions
  , hoverProvider                    = Just $ make True
  , signatureHelpProvider            = Just signatureHelpOptions
  , definitionProvider               = Just $ make definitionOptions
  , declarationProvider              = Just $ make False
  , typeDefinitionProvider           = Just $ make False
  , implementationProvider           = Just $ make False
  , referencesProvider               = Just $ make False
  , documentHighlightProvider        = Just $ make True
  , documentSymbolProvider           = Just $ make documentSymbolOptions
  , codeActionProvider               = Just $ make codeActionOptions
  , codeLensProvider                 = Just codeLensOptions
  , documentLinkProvider             = Just documentLinkOptions
  , colorProvider                    = Just $ make False
  , documentFormattingProvider       = Just $ make False
  , documentRangeFormattingProvider  = Just $ make False
  , documentOnTypeFormattingProvider = Nothing
  , renameProvider                   = Just $ make False
  , foldingRangeProvider             = Just $ make False
  , executeCommandProvider           = Just executeCommandOptions
  , selectionRangeProvider           = Just $ make False
  , linkedEditingRangeProvider       = Just $ make False
  , callHierarchyProvider            = Just $ make False
  , semanticTokensProvider           = Just $ make semanticTokensOptions
  , monikerProvider                  = Just $ make False
  , workspaceSymbolProvider          = Just $ make False
  , workspace                        = Just workspaceServerCapabilities
  , experimental                     = Nothing
  }

||| Server information to be sent to clients during the initialization protocol.
export
serverInfo : ServerInfo
serverInfo = MkServerInfo { name = "idris2-lsp", version = Just "0.1" }


text:
module Typedefs.Test.ReasonMLTests

import Typedefs.Names
import Typedefs.Typedefs
import Typedefs.Backend
import Typedefs.Backend.Utils
import Typedefs.Backend.ReasonML

import Typedefs.Test

import Text.PrettyPrint.WL
import Specdris.Spec

import Data.NEList
import Data.Vect

%access public export

x0 : Doc
x0 = text "'x0"

x1 : Doc
x1 = text "'x1"

x2 : Doc
x2 = text "'x2"

x3 : Doc
x3 = text "'x3"

eitherDoc : Doc
eitherDoc = text "type" |++| text "either" |+| tupled [x0,x1]
            |++| equals |++| text "Left" |+| parens x0 |++| pipe |++| text "Right" |+| parens x1 |+| semi

generate : TNamed n -> Maybe Doc
generate {n} tn = generateDefs ReasonML $ singleton (n ** tn)

testSuite : IO ()
testSuite = spec $ do

  describe "ReasonML code generation tests:" $ do
    let bitDoc = vsep2
                  [ preamble {def = ReasonML}
                  , eitherDoc
                  , text "type" |++| text "bit"
                    |++| equals |++| text "either" |+| tupled (replicate 2 (text "unit")) |+| semi
                  ]

    it "bit" $
      generate bit `shouldBe` (Just bitDoc)

    it "byte" $
      generate byte
        `shouldBe` (Just $ vsep2
                      [ bitDoc
                      , text "type" |++| text "byte"
                        |++| equals |++| tupled (replicate 8 (text "bit"))
                        |+| semi
                      ])

    let maybeDoc = vsep2
                     [ eitherDoc
                     , text "type" |++| text "maybe" |+| parens x0
                       |++| equals |++| text "either" |+| tupled [text "unit", x0]
                       |+| semi
                     ]

    it "maybe" $
      generate maybe `shouldBe` (Just $ vsep2 [preamble {def = ReasonML}, maybeDoc])

    let listDoc = text "type" |++| text "list" |+| parens x0
                  |++| equals |++| text "Nil"
                  |++| pipe   |++| text "Cons" |+| tupled [x0, text "list" |+| parens x0]
                  |+| semi

    it "list" $
      generate list `shouldBe` (Just $ vsep2 [preamble {def = ReasonML}, listDoc])

    let muMaybeDoc = text "type" |++| text "maybe2" |+| parens x0
                     |++| equals |++| text "Nothing"
                     |++| pipe   |++| text "Just" |+| parens x0
                     |+| semi

    it "maybe2" $
      generate maybe2 `shouldBe` (Just $ vsep2 [preamble {def = ReasonML}, muMaybeDoc])

    let natDoc = text "type" |++| text "nat"
                 |++| equals |++| text "Z"
                 |++| pipe   |++| text "S" |+| parens (text "nat")
                 |+| semi

    it "nat" $
      generate nat `shouldBe` (Just $ vsep2 [preamble {def = ReasonML}, natDoc])

    it "listNat" $
      generate listNat
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , natDoc
                      , text "type" |++| text "listNat"
                        |++| equals |++| text "NilN"
                        |++| pipe   |++| text "ConsN" |+| tupled [ text "nat", text "listNat" ]
                        |+| semi
                      ])

    it "parametricSynonym" $
      generate parametricSynonym
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , maybeDoc
                      , text "type" |++| text "parSyn" |+| parens x0
                        |++| equals |++| text "maybe" |+| parens x0
                        |+| semi
                      ])

    it "parametricSynonym2" $
      generate parametricSynonym2
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , muMaybeDoc
                      , text "type" |++| text "parSyn2" |+| parens x0
                        |++| equals |++| text "maybe2" |+| parens x0
                        |+| semi
                      ])

    it "aplusbpluscplusd" $
      generate aplusbpluscplusd
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , eitherDoc
                      , text "type" |++| text "aplusbpluscplusd" |+| tupled [x0,x1,x2,x3]
                        |++| equals |++| text "either" |+| tupled [x0,
                                            text "either" |+| tupled [x1,
                                              text "either" |+| tupled [x2, x3]]]
                        |+| semi
                      ])

    it "oneoneoneone" $
      generate oneoneoneone
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , eitherDoc
                      , text "type" |++| text "oneoneoneone"
                        |++| equals |++| text "either" |+| tupled [text "unit",
                                            text "either" |+| tupled [text "unit",
                                              text "either" |+| tupled [text "unit", text "unit"]]]
                        |+| semi
                      ])

    it "unusedFreeVars" $
      generate unusedFreeVars
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , text "type" |++| text "id" |+| parens x0
                        |++| equals |++| x0
                        |+| semi
                      ]) -- not "\ntype id('x0, 'x1, ..., 'x41) = 'x0\n"

    it "void or unit" $
      generate voidOrUnit
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , eitherDoc
                      , text "type" |++| text "void" |+| semi
                      , text "type" |++| text "voidOrUnit"
                        |++| equals |++| text "either" |+| tupled [text "void", text "unit"]
                        |+| semi
                      ])

    it "nonlinear variable usage" $
      generate nonlinear
        `shouldBe` (Just $ vsep2
                     [ preamble {def = ReasonML}
                     , text "type" |++| text "nonlinear" |+| parens x0
                       |++| equals |++| tupled [x0, x0]
                       |+| semi
                     ])

    it "nested Mu 1: List(Either(Alpha, Beta))" $
      generate nestedMu1
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , listDoc
                      , eitherDoc
                      , text "type" |++| text "nestedMu1" |+| tupled [x0,x1]
                        |++| equals |++| text "Foobar"
                                         |+| parens (text "list" |+| parens (text "either" |+| tupled [x0,x1]))
                        |+| semi
                      ])

    it "nested Mu 2: Maybe2(Alpha)" $
      generate nestedMu2
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , muMaybeDoc
                      , text "type" |++| text "nestedMu2" |+| parens x0
                        |++| equals |++| text "Foobar"
                                         |+| parens (text "maybe2" |+| parens x0)
                        |+| semi
                      ])

    it "nested Mu 3: Maybe2(Mu)" $
      generate nestedMu3
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}, muMaybeDoc
                      , text "type" |++| text "nestedMu3"
                        |++| equals |++| text "Foobar"
                                         |+| parens (text "maybe2" |+| parens (text "nestedMu3"))
                        |+| semi
                      ])

    let nestedMu4Doc =
      vsep2
        [ listDoc
        , eitherDoc
        , text "type" |++| text "nestedMu4" |+| parens x0
          |++| equals |++| text "Foobar"
                           |+| parens (text "list"
                                |+| parens (text "either"
                                     |+| tupled [ text "nestedMu4" |+| parens x0
                                                , x0 ]))
          |+| semi
        ]

    it "nested Mu 4: List(Either (Mu, Alpha))" $
      generate nestedMu4 `shouldBe` (Just $ vsep2 [preamble {def = ReasonML}, nestedMu4Doc])

    it "Nested mu 5: AnonList(Mu)" $
      generate nestedMu5
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}, text "type" |++| text "nilCons" |+| parens x0
                        |++| equals |++| text "Nil"
                        |++| pipe   |++| text "Cons"
                                         |+| tupled [ x0
                                                    , text "nilCons" |+| parens x0 ]
                        |+| semi
                      , text "type" |++| text "nestedMu5"
                        |++| equals |++| text "Foobar"
                                         |+| parens (text "nilCons" |+| parens (text "nestedMu5"))
                        |+| semi
                      ])

    it "nested Mu 6: NestedMu4(Maybe2(Either(Alpha, Nat)))" $
      generate nestedMu6
        `shouldBe` (Just $ vsep2
                      [ preamble {def = ReasonML}
                      , nestedMu4Doc
                      , muMaybeDoc
                      , natDoc
                      , text "type" |++| text "nestedMu6" |+| parens x0
                        |++| equals |++| text "Foobar"
                                         |+| parens (text "nestedMu4"
                                             |+| parens (text "maybe2"
                                                 |+| parens (text "either"
                                                     |+| tupled [ x0
                                                                , text "nat" ])))
                        |+| semi
                      ])

    it "list of definitions [bit, nibble, byte, char, hash, transitionId, data, previous, rootTx]" $
      generateDefs ReasonML listOfDefs
        `shouldBe` (Just $ vsep2
                      [ bitDoc
                      , text "type" |++| text "nibble"
                        |++| equals |++| tupled (replicate 4 (text "bit"))
                        |+| semi
                      , text "type" |++| text "byte"
                        |++| equals |++| tupled (replicate 2 (text "nibble"))
                        |+| semi
                      , text "type" |++| text "char"
                        |++| equals |++| text "byte"
                        |+| semi
                      , text "type" |++| text "hash"
                        |++| equals |++| text "byte"
                        |+| semi
                      , text "type" |++| text "transitionId"
                        |++| equals |++| text "byte"
                        |+| semi
                      , text "type" |++| text "data"
                        |++| equals |++| text "byte"
                        |+| semi
                      , text "type" |++| text "previous"
                        |++| equals |++| text "hash"
                        |+| semi
                      , text "type" |++| text "rootTx"
                        |++| equals |++| tupled [text "data", text "previous"]
                        |+| semi
                      ])

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module chap06

import Data.Vect

N : (n : Nat) -> Type
N n = (n : Nat ** Vect n Double)

Matrix : (n : Nat) -> (m : Nat) -> Type
Matrix n m = (m ** Vect m (N n))

AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next : Int) -> AdderType k

adder : (numargs : Nat) -> (acc : Int) -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

GenericAdderType : (numargs : Nat) -> Type -> Type
GenericAdderType Z numType = numType
GenericAdderType (S k) numType = (next : numType) -> GenericAdderType k numType

genericAdder : Num numType => (numargs : Nat) -> numType -> GenericAdderType numargs numType
genericAdder Z acc = acc
genericAdder (S k) acc = \next => genericAdder k (next + acc)

Position : Type
Position = (Double, Double)

Polygon : Nat -> Type
Polygon n = Vect n Position

tri : Polygon 3
tri = [(0, 0), (1, 1), (-1, -1)]
-- tri = [(?tri_rhs1, ?tri_rhs2), (?tri_rhs3, ?tri_rhs4), (?tri_rhs5, ?tri_rhs6)]

IntOrString : Bool -> Type
IntOrString False = String
IntOrString True = Int

-- dependent pattern matching
getIntOrString : (isInt : Bool) -> IntOrString isInt
getIntOrString False = "zero"
getIntOrString True = 0

-- converts either a String or an Int to a canonical String representation
valToString : (isInt : Bool) -> IntOrString isInt -> String
valToString False x = trim x
valToString True x = cast x

valToString' : (isInt : Bool) -> (case isInt of
                                       False => String
                                       True => Int) -> String
valToString' False x = trim x
valToString' True x = cast x