text:
module Idris.Codegen.ExtSTG.ANFToSTG

import public Idris.Codegen.ExtSTG.Core

import Compiler.ANF
import Core.Context
import Core.Core
import Core.TT
import Data.IOArray
import Libraries.Data.IntMap
import Data.List
import Libraries.Data.StringMap
import Data.Strings
import Data.Vect
import Idris.Codegen.ExtSTG.STG
import Idris.Codegen.ExtSTG.String
import Prelude
import Idris.Codegen.ExtSTG.StringTable
import Idris.Codegen.ExtSTG.PrimOp
import Idris.Codegen.ExtSTG.Erased
import Idris.Codegen.ExtSTG.ADTMap
import Idris.Codegen.ExtSTG.Foreign
import Idris.Codegen.ExtSTG.ExternalTopIds

import Debug.Trace

tracef : (Show b) => (a -> b) -> a -> a
tracef f a = trace (show (f a)) a

{-
Implementation notes

 * Idris primitive types are represented as Boxed values in STG. They are unboxed when they are applied to
   primitive operations, because primitive operations in STG work unboxed values. And they are unboxed
   when Idris' case expression matches on primitive values.
 * Handle of String literals from Idris to STG is different. In Idris ANF we can case match on string literals,
   but in STG it is not possible. In this case we have to generate a ifthenelse like embedded case matching
   for STG where the case scrutinee is a primitive operation to compare the value from the literal found
   in the case alternatives. Which introduces the next problem, string literals in STG are top-binders and
   they are represented as Addr# by the CMM. Having LitString with String is very misleading.
   So the points here:
   - When the code generator finds a String matcing case, it creates a top level bindings for String,
     which is considered as Addr#
   - When the Strings values are created, eg via readLine, they should do ByteArray allocations, which
     will be handled bye the garbage collector. When implementing a String Equality check (we must know
     the representation of the string OR just default back to Addr# ???)
     This step needs to be further checking TODO
   - String comparism primitive cStrCmp must be implemented in STG to solve this problem, this should a top
     level binding, whith a recursive function cStrCmp function.
   - The case chain which represents the ifthenelse chain should use the cStrCmp function.
 * Datatypes in STG and Idris ANF's IR are similar.
   - In STG datatypes are created by the STyCon which associates a type name with a Unique
     identifier and the list of data constructors SDataCon with their unique IDs too.
   - In ANF the data constructors and type constructors occupy the same namespace and the ones which
     are used only appear in the structure of the ANF program. This is not enough information for
     the STG backend to generate STG data type definitions.
   - Because there is only partial information in the ANF program, there is a need to look into
     the GlobalDef Context which is part of the Core compiler abstraction via `Ref Ctxt Defs`.
     From that source of information we have to remap type names and constructor names,
     which is currently done by a hack. All this detail can be found in the:
     TConsAndDCons namespace
   - TODO: Some words about matching data and type constructors
 * In ANF Erased values occupy arguments and they meant to be special values. In STG we create a
   simple data type with one constructor: Erased = Erased. During the ANF compilation when Erased in
   encuntered the corresponding value constructor in STG is referred.
 * TODO: Integer and String and AnyPtr
 * ...

TODOs
[+] Remove (Name, Name, Name) parameter from StgApp
[+] Add FC information to binders
[+] Write DataCon -> TypeCon association
[+] Separate STG Type and Term namespaces
[+] Fix mkDataConId
[+] Implement primitive values marshalled to the right GHC boxed primitives
[+] Implement Erased values, erased variables
[+] Generate StringTable for String literals
[.] Handle Data/Type constructors
    [+] Create StgConApp for data constructors
    [ ] Represent Type Constructors in unified datatype
    [ ] Match Type constructors in case expressions
[ ] Implement Crash primitive
[ ] Handle primitive case matches accordingly
[ ] Generate STG main entry
[.] Handle String matches with ifthenelse chains, using stringEq primop from STG
    [ ] Create a test program which reads from input.
[.] Implement primitive operations
    [ ] Implement casting
    [ ] ShiftL/ShiftR for Word needs a wrapper: Differences in parameters at STG and ANF side.
    [ ] DoubleFloor/Ceiling also needs a wrapper function as in STG the result is an Integer.
    [ ] Check if the BelieveMe operation is correct in STG
[*] Implement String handling STG code.
[ ] FFI calls AExtPrim
    [ ] Create a test program which FFI calls into a library.
    [ ] Foreign definitions should be looked up from a file, which can be modified by the user.
[ ] Module compilation
[+] FIX: Use StgCase instead of StgLet, otherwise strict semantics breaks.
[ ] Store defined/referred topLevelBinders
[+] Figure out how to use MkAlt with indexed types
[ ] Figure out the semantics for LazyReason in ANF Apps
[ ] ...
-}

||| Define an STG data type with one constructor.
definePrimitiveDataType
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => (String, String, Constant)
  -> Core ()
definePrimitiveDataType (u, m, StringType) = do
  logLine "Defining String datatype."
  -- defineDataType (MkUnitId u) (MkModuleName m) !IdrisString -- TODO
definePrimitiveDataType (u, m, c) = do
  t <- typeConNameForConstant c
  n <- dataConNameForConstant c
  d <- createSTyCon (t, SsUnhelpfulSpan t) [(n, AlgDataCon !(constantToPrimRep c), SsUnhelpfulSpan n)]
  defineDataType (MkUnitId u) (MkModuleName m) d

||| Create the primitive types section in the STG module.
|||
||| Idris primitive types are represented as boxed values in STG, with a datatype with one constructor.
||| Eg: data IdrInt = IdrInt #IntRep
definePrimitiveDataTypes
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => Core ()
definePrimitiveDataTypes = traverse_ definePrimitiveDataType
 [ ("ghc-prim", "GHC.Types",  IntType)
 , (MAIN_UNIT,  MAIN_MODULE,  IntegerType) -- TODO: This is bad, GMP Integer is needed here
 , ("base",     "GHC.Word",   Bits8Type)
 , ("base",     "GHC.Word",   Bits16Type)
 , ("base",     "GHC.Word",   Bits32Type)
 , ("base",     "GHC.Word",   Bits64Type)
 , ("ghc-prim", "GHC.Types",  CharType)
 , ("ghc-prim", "GHC.Types",  DoubleType)
-- , (MAIN_UNIT,  MAIN_MODULE,  StringType)
 , (MAIN_UNIT,  MAIN_MODULE,  WorldType)
 ]

-- TODO: Create ifthenelse chain for String literals
||| Compile constant for case alternative.
compileAltConstant : Constant -> Core Lit
compileAltConstant (I i)   = pure $ LitNumber LitNumInt $ cast i
compileAltConstant (BI i)  = pure $ LitNumber LitNumInt i -- ??? How to represent BIG integers ???
compileAltConstant (B8 i)  = pure $ LitNumber LitNumWord $ cast i
compileAltConstant (B16 i) = pure $ LitNumber LitNumWord $ cast i
compileAltConstant (B32 i) = pure $ LitNumber LitNumWord $ cast i
compileAltConstant (B64 i) = pure $ LitNumber LitNumWord64 i
compileAltConstant (Ch c)  = pure $ LitChar c
compileAltConstant (Db d)  = pure $ LitDouble d
compileAltConstant c = coreFail $ InternalError $ "compileAltConstant " ++ show c

||| Compile constant for APrimVal, Boxing a value in STG.
compileConstant : Constant -> Core Lit
compileConstant (I i)   = pure $ LitNumber LitNumInt $ cast i
compileConstant (BI i)  = pure $ LitNumber LitNumInt i -- ??? How to represent BIG integers ???
compileConstant (B8 i)  = pure $ LitNumber LitNumWord $ cast i
compileConstant (B16 i) = pure $ LitNumber LitNumWord $ cast i
compileConstant (B32 i) = pure $ LitNumber LitNumWord $ cast i
compileConstant (B64 i) = pure $ LitNumber LitNumWord64 i
compileConstant (Ch c)  = pure $ LitChar c
compileConstant (Db d)  = pure $ LitDouble d
compileConstant c = coreFail $ InternalError $ "compileConstant " ++ show c

data ValueConstant : Constant -> Type where
  IntConstant    : ValueConstant (I x)
  BigIntConstant : ValueConstant (BI x)
  Byte8Constant  : ValueConstant (B8 x)
  Byte16Constant : ValueConstant (B16 x)
  Byte32Constant : ValueConstant (B32 x)
  Byte64Constant : ValueConstant (B64 x)
  CharConstant   : ValueConstant (Ch x)
  DoubleConstant : ValueConstant (Db x)
  WorldConstant  : ValueConstant WorldVal

checkValueConstant : (c : Constant) -> Maybe (ValueConstant c)
checkValueConstant (I _)    = Just IntConstant
checkValueConstant (BI _)   = Just BigIntConstant
checkValueConstant (B8 _)   = Just Byte8Constant
checkValueConstant (B16 _)  = Just Byte16Constant
checkValueConstant (B32 _)  = Just Byte32Constant
checkValueConstant (B64 _)  = Just Byte64Constant
checkValueConstant (Ch _)   = Just CharConstant
checkValueConstant (Db _)   = Just DoubleConstant
checkValueConstant WorldVal = Just WorldConstant
checkValueConstant _        = Nothing

checkValueConstantM : (c : Constant) -> Core (ValueConstant c)
checkValueConstantM c = case checkValueConstant c of
  Nothing => coreFail $ InternalError $ "checkValueConstantM: " ++ show c ++ " is not a value constant."
  Just vc => pure vc

valueConstantPrimReps : (c : Constant) -> ValueConstant c => List PrimRep
valueConstantPrimReps (I _)    = [IntRep]
valueConstantPrimReps (BI _)   = [IntRep]
valueConstantPrimReps (B8 _)   = [Word8Rep]
valueConstantPrimReps (B16 _)  = [Word16Rep]
valueConstantPrimReps (B32 _)  = [Word32Rep]
valueConstantPrimReps (B64 _)  = [Word64Rep]
valueConstantPrimReps (Ch _)   = [Word8Rep]
valueConstantPrimReps (Db _)   = [DoubleRep]
valueConstantPrimReps WorldVal = []

valueConstantAlgDataCon : (c : Constant) -> ValueConstant c => DataConRep
valueConstantAlgDataCon c = AlgDataCon (valueConstantPrimReps c)

valueConstantName : (c : Constant) -> ValueConstant c => String
valueConstantName (I _)    = "I#"
valueConstantName (BI _)   = "GMPInt"
valueConstantName (B8 _)   = "W8#"
valueConstantName (B16 _)  = "W16#"
valueConstantName (B32 _)  = "W32#"
valueConstantName (B64 _)  = "W64#"
valueConstantName (Ch _)   = "C#"
valueConstantName (Db _)   = "D#"
valueConstantName WorldVal = "IdrWorld"

||| Determine the Data constructor for the boxed primitive value.
||| Used in creating PrimVal
|||
||| The name of terms should coincide the ones that are defined in GHC's ecosystem. This
||| would make the transition easier, I hope.
dataConIdForValueConstant
  :  DataTypeMapRef => UniqueMapRef => Ref Counter Int
  => (c : Constant) -> ValueConstant c => Core DataConIdSg
dataConIdForValueConstant c = mkDataConIdStr (valueConstantName c)

tyConIdForValueConstant : UniqueMapRef => Ref Counter Int => FC -> Constant -> Core TyConId
tyConIdForValueConstant _ (I _)    = tyConIdForConstant IntType
tyConIdForValueConstant _ (BI _)   = tyConIdForConstant IntegerType
tyConIdForValueConstant _ (B8 _)   = tyConIdForConstant Bits8Type
tyConIdForValueConstant _ (B16 _)  = tyConIdForConstant Bits16Type
tyConIdForValueConstant _ (B32 _)  = tyConIdForConstant Bits32Type
tyConIdForValueConstant _ (B64 _)  = tyConIdForConstant Bits64Type
tyConIdForValueConstant _ (Ch _)   = tyConIdForConstant CharType
tyConIdForValueConstant _ (Db _)   = tyConIdForConstant DoubleType
tyConIdForValueConstant _ WorldVal = tyConIdForConstant WorldType
tyConIdForValueConstant fc other   = coreFail $ InternalError $ "tyConIdForValueConstant " ++ show other ++ ":" ++ show fc

primTypeForValueConstant : UniqueMapRef => Ref Counter Int => FC -> Constant -> Core PrimRep
primTypeForValueConstant _ (I _)    = pure IntRep
primTypeForValueConstant _ (BI _)   = pure IntRep
primTypeForValueConstant _ (B8 _)   = pure Word8Rep
primTypeForValueConstant _ (B16 _)  = pure Word16Rep
primTypeForValueConstant _ (B32 _)  = pure Word32Rep
primTypeForValueConstant _ (B64 _)  = pure Word64Rep
primTypeForValueConstant _ (Ch _)   = pure Word8Rep
primTypeForValueConstant _ (Db _)   = pure DoubleRep
primTypeForValueConstant fc other   = coreFail $ InternalError $ "primTypeForValueConstant " ++ show other ++ ":" ++ show fc

createAlternatives
  : (r : RepType) -> List (Lit, Expr Core.stgRepType) -> Maybe (List (Alt r Core.stgRepType))
createAlternatives r [] = Just []
createAlternatives r ((l,b) :: ls) = do
  Refl <- decLitRepType l r
  a    <- decAltLit l
  map ((MkAlt (AltLit l) () b) ::) $ createAlternatives r ls

mutual
  compileANF
    : UniqueMapRef => Ref Counter Int => Ref ADTs ADTMap => StringTableRef
    => Ref Ctxt Defs => DataTypeMapRef
    => Core.Name.Name -> ANF
    -> Core (Expr Core.stgRepType)
  compileANF funName (AV fc var)
    = pure $ StgApp !(mkBinderIdVar fc funName Core.stgRepType var) [] stgRepType

  -- TODO: Figure out the semantics for LazyReason
  compileANF funToCompile (AAppName fc lazyReason funToCall args)
    = pure $ StgApp !(mkBinderIdName funToCall)
                    !(traverse (mkStgArg fc funToCompile) args)
                    stgRepType

  compileANF funToCompile (AUnderApp fc funToCall _ args)
    = pure $ StgApp !(mkBinderIdName funToCall)
                    !(traverse (mkStgArg fc funToCompile) args)
                    stgRepType

  -- TODO: Figure out the semantics for LazyReason
  compileANF funName (AApp fc lazyReason closure arg)
    = pure $ StgApp !(mkBinderIdVar fc funName Core.stgRepType closure)
                    [!(mkStgArg fc funName arg)]
                    stgRepType

  compileANF funName (ALet fc var expr body) = do
    pure
      $ StgCase
          PolyAlt -- It could be ForceUnbox, and only AltDefault should be used in Strict Let
          !(compileANF funName expr)
          !(mkSBinderLocal fc funName var)
          [ MkAlt AltDefault () !(compileANF funName body) ]

  -- TODO: Implement
  -- TODO: Use the ConInfo if possible
  compileANF _ acon@(ACon fc name coninfo Nothing args) = do
    -- Types probably will be represented with one STG TyCon and DataCon
    -- for every type.
    coreFail $ InternalError $ "Figure out how to represent a type as a value!"

  compileANF funName acon@(ACon fc name coninfo (Just tag) args) = do
    -- Lookup the constructor based on the name.
    -- The tag information is not relevant here.
    -- Args are variables
    (rep ** dataConId) <- mkDataConId name
    conArgs <- compileConArgs fc funName args rep
    pure $ StgConApp dataConId conArgs

  -- TODO: Figure out the semantics for LazyReason
  compileANF funName (AOp fc lazyReason prim args)
    = compilePrimOp fc funName prim args

  -- TODO: Implement
  -- TODO: Figure out the semantics for LazyReason
  compileANF _ aext@(AExtPrim _ lazyReason name args) = do
    logLine $ "To be implemented: " ++ show aext
    pure
      $ StgApp (!(mkBinderIdStr STRING_FROM_ADDR))
               [ mkArgSg $ StgLitArg $ LitString $ "AExtPrim " ++ show name ++ " " ++ show args
               ]
               (SingleValue LiftedRep)

  compileANF funName (AConCase fc scrutinee alts mdef) = do
    -- Compute the alt-type
    tyCon <- do
      -- Lookup the STyCon definition from the alt names
      namesAndTyCons
        <- traverse
            (\(MkAConAlt name coninfo tag args body) => map (name,) (lookupTyCon name))
            alts
      -- Check if there is exactly one STyCon definition is found
      [] <- pure $ mapMaybe
                    (\(n,x) => case x of { Nothing => Just n; _ => Nothing})
                    namesAndTyCons
        | nonDefinedConstructors => coreFail $ InternalError $ unlines $
            "Constructors not having type information: " :: map show nonDefinedConstructors
      case mapMaybe snd namesAndTyCons of
        []  => coreFail $ InternalError $ "No type constructor is found for: " ++ show fc
        [t] => pure $ STyCon.Id t
        ts  => case nub (map STyCon.Id ts) of
                 []  => coreFail $ InternalError "Impossible case in compile AConCase"
                 [t] => pure t
                 ts  => coreFail $ InternalError $ "More than TyCon found for: " ++ show fc
    scrutBinder <- mkBinderIdVar fc funName Core.stgRepType scrutinee
    let stgScrutinee = StgApp scrutBinder [] stgRepType
    caseBinder <- mkFreshSBinderStr LocalScope fc "conCaseBinder"
    stgDefAlt <- maybe
      (pure [])
      (\x => do
        stgBody <- compileANF funName x
        pure [MkAlt AltDefault () stgBody])
      mdef
    stgAlts <- traverse (compileConAlt fc funName) alts
    pure $ StgCase (AlgAlt tyCon) stgScrutinee caseBinder (stgDefAlt ++ stgAlts)

  compileANF funName (AConstCase fc scrutinee alts mdef) = do
    let checkStringAlt : AConstAlt -> Bool
        checkStringAlt (MkAConstAlt (Str _) _) = True
        checkStringAlt _                       = False
    let getAltConstant : AConstAlt -> Constant
        getAltConstant (MkAConstAlt c _) = c
    case partition checkStringAlt alts of
      -- No String alts
      ([], []) => coreFail $ InternalError "Empty alternatives..."
      ([], alts@(alt::_)) => do
        [tyCon] <- map nub $ traverse (tyConIdForValueConstant fc . getAltConstant) alts
          | ts => coreFail $ InternalError $ "Constant case found " ++ show (length ts) ++ " type constructors in " ++ show fc
        let altConstant = getAltConstant alt
        valueConst <- checkValueConstantM altConstant
        ((AlgDataCon [rep]) ** dtCon) <- dataConIdForValueConstant altConstant
          | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show (fc, funName, wrongRep)
        primVal <- mkFreshSBinderRepStr LocalScope (SingleValue rep) fc "primVal"
        litBodies
          <- traverse
              \case
                (MkAConstAlt c b) => do
                  lit <- compileAltConstant c
                  body <- compileANF funName b
                  pure (lit, body)
              alts
        let Just stgAlts = createAlternatives (SingleValue rep) litBodies
            | Nothing => coreFail
                       $ InternalError
                       $ "Representation in literal types were different then expexted:" ++ show (rep, map fst litBodies)
        stgDefAlt <- maybe
          (pure [])
          (\x => do
            stgBody <- compileANF funName x
            pure [the (Alt (SingleValue rep) Core.stgRepType) (MkAlt AltDefault () stgBody)])
          mdef
        -- stgAlts <- traverse (compileConstAlt funName) alts
        pure
          $ StgCase
              (AlgAlt tyCon)
              (StgApp !(mkBinderIdVar fc funName Core.stgRepType scrutinee) [] stgRepType)
              !nonused
              [ MkAlt (AltDataCon (mkDataConIdSg dtCon)) primVal
              $ StgCase
                  (PrimAlt rep)
                  (StgApp (binderId primVal) [] (SingleValue rep))
                  !(nonusedRep (SingleValue rep))
                  (stgDefAlt ++ stgAlts)
              ]

      -- String alts
      (strAlts, []) => do

        mStgDef <- traverseOpt (compileANF funName) mdef
        scrutBinder <- mkBinderIdVar fc funName Core.stgRepType scrutinee

        -- TODO: Make this typesafe
        let caseChain : List AConstAlt -> Core (Expr Core.stgRepType)
            caseChain [] = coreFail $ InternalError "Impossible, empty string alternatives."
            caseChain [MkAConstAlt (Str s) body] = do
              stringLit             <- mkFreshSBinderStr LocalScope fc "stringLitBinder"
              stringEqResult        <- mkFreshSBinderStr LocalScope fc "stringEqResult"
              unusedBinder          <- mkFreshSBinderRepStr LocalScope (SingleValue IntRep) fc "unusedBinder"
              stringEqResultUnboxed <- mkFreshSBinderRepStr LocalScope (SingleValue IntRep) fc "stringEqResultUnboxed"
              sBinderId <- registerString fc s
              ((AlgDataCon [IntRep]) ** ti) <- dataConIdForConstant IntType
                | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show (fc, funName, wrongRep)
              pure $
                -- Look up the string from the string table.
                StgCase
                  (AlgAlt !idrisStringTyConId)
                  (StgApp !stringFromAddrBinderId2 [mkArgSg $ StgVarArg sBinderId] (SingleValue LiftedRep))
                  stringLit
                  [ MkAlt AltDefault ()
                    -- Call the strEq function
                  $ StgCase
                      (AlgAlt !(tyConIdForConstant IntType))
                      (StgApp !(mkBinderIdStr "Idris.String.strEq")
                              [ mkArgSg $ StgVarArg $ scrutBinder
                              , mkArgSg $ StgVarArg $ binderId stringLit ]
                              stgRepType)
                      stringEqResult
                      [ MkAlt (AltDataCon (mkDataConIdSg ti)) stringEqResultUnboxed $
                              -- Unbox the result
                              StgCase
                                (PrimAlt IntRep)
                                (StgApp (binderId stringEqResultUnboxed) [] (SingleValue IntRep))
                                unusedBinder
                                $ catMaybes
                                  [ -- Match on False: call default
                                    (MkAlt AltDefault ()) <$> mStgDef
                                  , -- Match on True: call body
                                    Just $ MkAlt (AltLit (LitNumber LitNumInt 1)) ()
                                                 !(compileANF funName body)
                                  ]
                      ]
                  ]
            caseChain ((MkAConstAlt (Str s) body) :: rest) = do
              stringLit             <- mkFreshSBinderStr LocalScope fc "stringLitBinder"
              stringEqResult        <- mkFreshSBinderStr LocalScope fc "stringEqResult"
              unusedBinder          <- mkFreshSBinderRepStr LocalScope (SingleValue IntRep) fc "unusedBinder"
              stringEqResultUnboxed <- mkFreshSBinderRepStr LocalScope (SingleValue IntRep) fc "stringEqResultUnboxed"
              sBinderId <- registerString fc s
              ((AlgDataCon [IntRep]) ** ti) <- dataConIdForConstant IntType
                | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show (fc, funName, wrongRep)
              pure $
                -- Look up the string from the string table.
                StgCase
                  (AlgAlt !idrisStringTyConId)
                  (StgApp !stringFromAddrBinderId2 [mkArgSg $ StgVarArg sBinderId] (SingleValue LiftedRep))
                  stringLit
                  [ MkAlt AltDefault ()
                    -- Call the strEq function
                  $ StgCase
                      (AlgAlt !(tyConIdForConstant IntType))
                      (StgApp !(mkBinderIdStr "Idris.String.strEq")
                              [ mkArgSg $ StgVarArg scrutBinder
                              , mkArgSg $ StgVarArg $ binderId stringLit
                              ]
                              stgRepType)
                      stringEqResult
                      [ MkAlt (AltDataCon (mkDataConIdSg ti)) stringEqResultUnboxed $
                              -- Unbox the result
                              StgCase
                                (PrimAlt IntRep)
                                (StgApp (binderId stringEqResultUnboxed) [] (SingleValue IntRep))
                                unusedBinder
                                $ -- Match on False: check the next alternative
                                  [ MkAlt AltDefault () !(caseChain rest)
                                    -- Match on True: call body
                                  , MkAlt (AltLit (LitNumber LitNumInt 1)) ()
                                           !(compileANF funName body)
                                  ]
                      ]
                  ]
            caseChain ((MkAConstAlt _ _)::_) =
              coreFail $ InternalError "Impossible, not expected non-string literal."
        caseChain strAlts

      -- Mixed alternatives
      _ => coreFail $ InternalError $ "Mixed string and non-string constant alts" ++ show fc

  compileANF _ (APrimVal fc (Str str)) = do
    topLevelBinder <- registerString fc str
    stringAddress  <- mkFreshSBinderRepStr LocalScope (SingleValue AddrRep) fc "stringPrimVal"
    pure $ StgCase
            (PrimAlt AddrRep)
            (StgApp topLevelBinder [] (SingleValue AddrRep)) -- TODO: Is this right?
            stringAddress
            [ MkAlt AltDefault ()
            $ StgApp
                (snd !stringFromAddrBinderId)
                [ mkArgSg $ StgVarArg $ binderId stringAddress ]
                stgRepType
            ]

  compileANF _ (APrimVal fc WorldVal) = do
    (AlgDataCon [] ** dataConId) <- dataConIdForValueConstant WorldVal
      | other => coreFail $ InternalError $ show (fc,WorldVal) ++ " has different representation: " ++ show other
    pure $ StgConApp dataConId ()

  compileANF _ (APrimVal fc c) = do
    -- TODO: Handle WorldVal
    valueConstant <- checkValueConstantM c
    (AlgDataCon [rep] ** dataConId) <- dataConIdForValueConstant c
      | other => coreFail $ InternalError $ show (fc,c) ++ " has different representation: " ++ show other
    lit <- compileConstant c
    same <- checkSemiDecEq ("compileANF " ++ show (fc, c)) (SingleValue rep) (litRepType lit)
    pure $ StgConApp dataConId (StgLitArg lit)

  compileANF _ (AErased fc)
    = do sbinder <- mkSBinderStr fc ERASED_TOPLEVEL_NAME
         pure $ StgApp (binderId sbinder) [] (SingleValue LiftedRep)

  -- TODO: Implement: Use Crash primop. errorBlech2 for reporting error ("%s", msg)
  compileANF _ ac@(ACrash _ msg) = do
    logLine $ "To be implemented: " ++ show ac
    pure
      $ StgApp (!(mkBinderIdStr STRING_FROM_ADDR))
               [ mkArgSg $ StgLitArg $ LitString $ "ACrash " ++ msg
               ]
               (SingleValue LiftedRep)

  mkArgList
    :  UniqueMapRef => Ref Counter Int => Ref ADTs ADTMap
    => FC -> Name.Name -> List AVar -> (ps : List PrimRep) -> Core (ArgList ps)
  mkArgList _ _ [] [] = pure []
  mkArgList f n (a::as) (r::rs) = do
    arg <- map StgVarArg $ mkBinderIdVar f n (SingleValue r) a
    args <- mkArgList f n as rs
    pure (arg :: args)
  mkArgList _ _ _ _ = coreFail $ InternalError "mkArgList: inconsistent state."

  compileConArgs
    :  UniqueMapRef => Ref Counter Int => Ref ADTs ADTMap
    => FC -> Name.Name -> List AVar -> (r : DataConRep)
    -> Core (StgConAppArgType r)
  compileConArgs fc funName _   (UnboxedTupleCon _)
    = coreFail $ InternalError "compileConArgs: UnboxedTupleCon"
  compileConArgs fc funName []  (AlgDataCon [])
    = pure ()
  compileConArgs fc funName [a] (AlgDataCon [r])
    = StgVarArg <$> mkBinderIdVar fc funName (SingleValue r) a
  compileConArgs fc funName (a0 :: a1 :: as) (AlgDataCon (r0 :: r1 :: rs))
    = mkArgList fc funName (a0 :: a1 :: as) (r0 :: r1 :: rs)
  compileConArgs _ _ _ _ = coreFail $ InternalError "compileConArgs: inconsistent state #2"

  createConAltBinders
    :  UniqueMapRef => Ref Counter Int => Ref ADTs ADTMap
    => FC -> Core.Name.Name -> List Int -> (ps : List PrimRep)
    -> Core (BList ps)
  createConAltBinders fc funName [] [] = pure []
  createConAltBinders fc funName (i :: is) (p :: ps) = do
    x <- mkSBinderRepLocal (SingleValue p) fc funName i
    xs <- createConAltBinders fc funName is ps
    pure (x :: xs)
  createConAltBinders fc funName is ps = coreFail $ InternalError $ "createConAltBinders found irregularities: " -- ++ show (is,ps)

  compileConAltArgs
    :  UniqueMapRef => Ref Counter Int => Ref ADTs ADTMap
    => FC -> Core.Name.Name -> List Int -> (r : DataConRep)
    -> Core (DataConRepType r)
  compileConAltArgs fc funName _   (UnboxedTupleCon _)
    = coreFail $ InternalError $ "Encountered UnboxedTuple when compiling con alt: " ++ show (funName, fc)
  compileConAltArgs fc funName []  (AlgDataCon [])    = pure ()
  compileConAltArgs fc funName [i] (AlgDataCon [rep]) = mkSBinderRepLocal (SingleValue rep) fc funName i
  compileConAltArgs fc funName (i0 :: i1 :: is) (AlgDataCon (r0 :: r1 :: rs))
    = createConAltBinders fc funName (i0 :: i1 :: is) (r0 :: r1 :: rs)
  compileConAltArgs fc funname is alt
    = coreFail $ InternalError $ "Encountered irregularities " -- ++ show (is, alt)

  compileConAlt
    : UniqueMapRef => Ref Counter Int => Ref ADTs ADTMap
    => StringTableRef => Ref Ctxt Defs => DataTypeMapRef
    => FC -> Core.Name.Name -> AConAlt
    -> Core (Alt (SingleValue LiftedRep) Core.stgRepType)
  compileConAlt fc funName c@(MkAConAlt name coninfo Nothing args body) = do
    coreFail $ InternalError $ "Figure out how to do pattern match on type: " ++ show name
  compileConAlt fc funName c@(MkAConAlt name coninfo (Just tag) args body) = do
    stgBody     <- compileANF funName body
    stgDataCon  <- mkDataConId name
    stgArgs     <- compileConAltArgs fc funName args (fst stgDataCon)
    pure $ MkAlt (AltDataCon stgDataCon) stgArgs stgBody

compileTopBinding
  :  UniqueMapRef
  => Ref Counter Int
  => Ref Ctxt Defs
  => StringTableRef
  => Ref ADTs ADTMap
  => Ref ExternalBinder ExtBindMap
  => DataTypeMapRef
  => (Core.Name.Name, ANFDef)
  -> Core (Maybe TopBinding)
compileTopBinding (funName,MkAFun args body) = do
--  logLine $ "Compiling: " ++ show funName
  funBody       <- compileANF funName body
  funArguments  <- traverse (map mkSBinderSg . mkSBinderLocal emptyFC funName) args
  funNameBinder <- mkSBinderName emptyFC funName
  rhs           <- pure $ StgRhsClosure ReEntrant funArguments funBody
  -- Question: Is Reentrant OK here?
  -- TODO: Calculate Rec or NonRec
  binding       <- pure $ StgRec [(funNameBinder,rhs)]
  -- Question: Is non-recursive good here? Test it.
  pure $ Just $ StgTopLifted binding
compileTopBinding (name,con@(MkACon aname tag arity)) = do
  -- logLine $ "TopLevel MkACon: " ++ show (name, aname, con)
  -- Covered in the LearnDataTypes section
  pure Nothing
compileTopBinding (name,MkAForeign css fargs rtype) = do
  -- logLine $ "Found foreign: " ++ show name
  map Just $ foreign name css fargs rtype
compileTopBinding (name,MkAError body) = do
  logLine $ "Skipping error: " ++ show name
  pure Nothing

groupExternalTopIds
  :  List (UnitId, ModuleName, SBinderSg)
  -> List (UnitId, List (ModuleName, List SBinderSg))
groupExternalTopIds = resultList . unionsMap . map singletonMap
  where
    EntryMap : Type
    EntryMap = StringMap (StringMap (List SBinderSg))

    resultList : EntryMap -> List (UnitId, List (ModuleName, List SBinderSg))
    resultList
      = map (bimap MkUnitId (map (mapFst MkModuleName) . toList))
      . toList

    unionsMap : List EntryMap -> EntryMap
    unionsMap = foldl (mergeWith (mergeWith (++))) empty

    singletonMap : (UnitId, ModuleName, SBinderSg) -> EntryMap
    singletonMap (MkUnitId n, MkModuleName m, sbinder) = singleton n (singleton m [sbinder])

partitionBy : (a -> Either b c) -> List a -> (List b, List c)
partitionBy f [] = ([], [])
partitionBy f (x :: xs) =
  let (bs, cs) = partitionBy f xs
  in case f x of
      (Left b)  => (b :: bs, cs)
      (Right c) => (bs, c :: cs)

defineMain : UniqueMapRef => Ref Counter Int => Core TopBinding
defineMain = do
  main <- mkSBinderExtId emptyFC "main"
  voidArg <- mkSBinderRepLocalStr (SingleValue VoidRep) "mainVoidArg"
  progMain <- mkSBinderTopLevel "{__mainExpression:0}"
  pure
    $ topLevel main [mkSBinderSg voidArg]
    $ StgApp (binderId progMain) [] stgRepType

-- We compile only one enormous module
export
compileModule
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> {auto _ : DataTypeMapRef}
  -> {auto _ : StringTableRef}
  -> {auto _ : Ref Ctxt Defs}
  -> {auto _ : Ref ExternalBinder ExtBindMap}
  -> List (Core.Name.Name, ANFDef)
  -> Core Module
compileModule anfDefs = do
  adts <- mkADTs
  registerHardcodedExtTopIds
  definePrimitiveDataTypes
  defineErasedADT
  createDataTypes
  defineStringTypes
  let phase              = "Main"
  let moduleUnitId       = MkUnitId "main"
  let name               = MkModuleName "Main" -- : ModuleName
  let sourceFilePath     = "some.idr" -- : String
  let foreignStubs       = NoStubs -- : ForeignStubs -- ???
  let hasForeignExported = False -- : Bool
  let dependency         = [] -- : List (UnitId, List ModuleName)
  mainTopBinding         <- defineMain
  erasedTopBinding       <- erasedTopBinding
  strFunctions1          <- String.stgTopBindings
  strFunctions2          <- catMaybes <$> traverse compileTopBinding topLevelANFDefs
  let stringTopBindings = strFunctions1 ++ strFunctions2
  compiledTopBindings    <- catMaybes <$> traverse compileTopBinding anfDefs
  stringTableBindings    <- StringTable.topLevelBinders
  let topBindings        = mainTopBinding ::
                           erasedTopBinding ::
                           stringTopBindings ++
                           stringTableBindings ++
                           compiledTopBindings
  tyCons                 <- getDefinedDataTypes -- : List (UnitId, List (ModuleName, List tcBnd))
  let foreignFiles       = [] -- : List (ForeignSrcLang, FilePath)
  externalTopIds0        <- genExtTopIds
  let externalTopIds     = groupExternalTopIds externalTopIds0
  pure $ MkModule
    phase
    moduleUnitId
    name
    sourceFilePath
    foreignStubs
    hasForeignExported
    dependency
    externalTopIds
    tyCons
    topBindings
    foreignFiles

{-
RepType: How doubles are represented? Write an example program: Boxed vs Unboxed
https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Builtin/primops.txt.pp
-}

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Flexidisc.OrdList.CompWithKeys

import Flexidisc.OrdList.Sub
import Flexidisc.OrdList.Type

import public Data.List

%default total

||| Proof that an `Ordlist` is composed of the given keys and another `OrdList`.
|||
||| Used in `discard`, probably not useful anywhere else.
public export
data CompWithKeys : (keys : List k) -> (xs, ys : OrdList k v o) -> Type where
  ||| Both `OrdList`s are empty
  Empty : CompWithKeys [] [] []
  ||| The second `OrdList` contains an extra key, that is not in the first `OrdList`
  Skip  : (loc : Elem k keys) -> CompWithKeys (dropElem keys loc) xs ys ->
          CompWithKeys keys xs (y::ys)
  ||| An element is shared bit both `OrdList`s
  Keep  : CompWithKeys keys xs ys -> CompWithKeys keys ((k, ty)::xs) ((k, ty)::ys)

%name CompWithKeys sub, issub, ss

||| Map a `CompWithKeys` to a `Sub`
export
toSub : CompWithKeys keys xs ys -> Sub xs ys
toSub Empty        = Empty
toSub (Skip x sub) = Skip (toSub sub)
toSub (Keep sub)   = Keep (toSub sub)

ext: idr

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
import Data.So

fromString : String -> Either String Nat
fromString = Left

fromInteger : (x : Integer) -> (0 _ : So (x >= 0)) => Either String Nat
fromInteger x = Right $ integerToNat x

x : List $ Either String Nat
x = ["x", 1, 2, "y"]

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Language.LSP.CodeAction.MakeLemma

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.List1
import Data.String
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Resugar
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Parser.Unlit
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.TTImp
import TTImp.Interactive.MakeLemma

buildCodeAction : Name -> URI -> List TextEdit -> CodeAction
buildCodeAction name uri edits =
  let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri edits)
                                      , documentChanges   = Nothing
                                      , changeAnnotations = Nothing
                                      }
   in MkCodeAction { title       = "Make lemma of \{show name}"
                   , kind        = Just RefactorExtract
                   , diagnostics = Just []
                   , isPreferred = Just False
                   , disabled    = Nothing
                   , edit        = Just workspaceEdit
                   , command     = Nothing
                   , data_       = Nothing
                   }

findBlankLine : List String -> Int -> Int
findBlankLine [] acc = acc
findBlankLine (x :: xs) acc = if trim x == "" then acc else findBlankLine xs (acc - 1)

export
makeLemma : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => CodeActionParams -> Core (Maybe CodeAction)
makeLemma params = do
  let True = params.range.start.line == params.range.end.line
    | _ => do logString Debug "makeLemma: start and end line were different"
              pure Nothing

  [] <- searchCache params.range MakeLemma
    | action :: _ => do logString Debug "makeLemma: found cached action"
                        pure (Just action)

  nameLocs <- gets MD nameLocMap
  let line = params.range.start.line
  let col = params.range.start.character
  let Just (loc@(_, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => do logString Debug "makeLemma: couldn't find name at \{show (line, col)}"
                    pure Nothing

  context <- gets Ctxt gamma
  toBeBracketed <- gets Syn bracketholes
  let toBrack = elemBy (\x, y => dropNS x == dropNS y) name toBeBracketed

  [(n, nidx, Hole locs _, ty)] <- lookupNameBy (\g => (definition g, type g)) name context
    | _ => do logString Debug $ "makeLemma: \{show name} is not a metavariable"
              pure Nothing

  (lty, lapp) <- makeLemma replFC name locs ty
  lemmaTy <- pterm lty
  papp <- pterm lapp
  let lemmaApp = show $ the PTerm $ if toBrack then addBracket replFC papp else papp

  src <- lines <$> getSource
  let Just srcLine = elemAt src (integerToNat (cast line))
    | Nothing => do logString Debug $ "makeLemma: error while fetching the referenced line"
                    pure Nothing
  let (markM, _) = isLitLine srcLine
  -- TODO: currently it has the same behaviour of the compiler, it puts the new
  --       definition in the first blank line above the hole. We want to put it
  --       exactly above the clause or declaration that uses the hole, however
  --       this information is needed within the compiler, so waiting future PRs.
  let blank = findBlankLine (reverse $ take (integerToNat (cast line)) src) line

  let appEdit = MkTextEdit (MkRange (uncurry MkPosition nstart) (uncurry MkPosition nend)) lemmaApp
  let tyEdit = MkTextEdit (MkRange (MkPosition blank 0) (MkPosition blank 0))
                          (relit markM "\{show $ dropNS name} : \{show lemmaTy}\n\n")
  let action = buildCodeAction name params.textDocument.uri [tyEdit, appEdit]
  modify LSPConf (record { cachedActions $= insert (cast loc, MakeLemma, [action]) })
  pure $ Just action


text:
> %default total
> %auto_implicits off

> X : Type
> H : Type
> fulfils : X -> H -> Bool

> LTE : H -> H -> Type
> LTE h1 h2 = (x : X) -> fulfils x h1 = True -> fulfils x h2 = True

> antisymmetricLTE : (h1 : H) -> (h2 : H) -> h1 `LTE` h2 -> h2 `LTE` h1 ->
>                    (x : X) -> fulfils x h1 = fulfils x h2
> antisymmetricLTE h1 h2 p q y with (fulfils y h1)
>   | True  = ?kika
>   | False = ?kiko

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Books.Comic

export
comicBook : String
comicBook = "Comic book"


text:
module Data.Scientific

import Data.Fin
import Data.List
import Data.Vect

||| Arbitrary precision coefficient for scientific notation in base b.
||| Representants are unique regarding (==) and there are no trailing zeros.
||| For a coefficient x this holds:
|||   1 <= x < b
public export
data Coefficient : (b : Nat) -> Type where
  CoeffInt : Fin (S b) ->
             Coefficient (S (S b))
  CoeffFloat : Fin (S b) ->
               List (Fin (S (S b))) ->
               Fin (S b) ->
               Coefficient (S (S b))

public export
Uninhabited (Coefficient 0) where
  uninhabited _ impossible
public export
Uninhabited (Coefficient 1) where
  uninhabited _ impossible

public export
Eq (Coefficient b) where
  (CoeffInt x) == (CoeffInt y) = x == y
  (CoeffFloat x xs x') == (CoeffFloat y ys y') = x == y && xs == ys && x' == y'
  _ == _ = False

public export
Ord (Coefficient b) where
  compare (CoeffInt x) (CoeffInt y) = compare x y
  compare (CoeffInt x) (CoeffFloat y ys y') = case compare x y of
                                               EQ => LT
                                               comp => comp
  compare (CoeffFloat x xs x') (CoeffInt y) = case compare x y of
                                               EQ => GT
                                               comp => comp
  compare (CoeffFloat x xs x') (CoeffFloat y ys y') =
    compare (FS x :: xs `snoc` FS x') (FS y :: ys `snoc` FS y')

private
prettyShowDigit : Fin 10 -> Char
prettyShowDigit x =
  case x of
       0 => '0'
       1 => '1'
       2 => '2'
       3 => '3'
       4 => '4'
       5 => '5'
       6 => '6'
       7 => '7'
       8 => '8'
       9 => '9'

private
prettyShowCoefficient : Coefficient 10 -> String
prettyShowCoefficient (CoeffInt x) = pack [ prettyShowDigit (FS x) ]
prettyShowCoefficient (CoeffFloat x xs x') =
  pack $ [ prettyShowDigit (FS x), '.' ] ++ map prettyShowDigit xs ++ [ prettyShowDigit (FS x') ]

public export
data Sign = Positive
          | Negative

public export
Eq Sign where
  Positive == Positive = True
  Negative == Negative = True
  _ == _ = False

public export
Ord Sign where
  compare Positive Positive = EQ
  compare Positive Negative = GT
  compare Negative Positive = LT
  compare Negative Negative = EQ

private
prettyShowSign : Sign -> String
prettyShowSign s = case s of
                        Positive => ""
                        Negative => "-"

||| A scientific notation numeral in base b.
||| Representants are unique, as this type is built on top of Coefficient.
||| The numbers x represented are those which can be written as a finite sum of powers of b:
|||   x = \Sigma_{i=n}^m a_i * b^i          , {n,m : Integer; a_i : Fin b}
public export
data Scientific : (b : Nat) -> Type where
  SciZ : Scientific (S (S b))
  Sci : Sign ->
        Coefficient b ->
        Integer ->
        Scientific b

public export
Uninhabited (Scientific 0) where
  uninhabited (Sci _ _ _) impossible

public export
Uninhabited (Scientific 1) where
  uninhabited (Sci _ _ _) impossible

public export
Eq (Scientific b) where
  SciZ == SciZ = True
  (Sci s c e) == (Sci s' c' e') = s == s' && c == c' && e == e'
  _ == _ = False

public export
Ord (Scientific b) where
  compare SciZ SciZ = EQ
  compare SciZ (Sci s _ _) = case s of
                                  Positive => LT
                                  Negative => GT
  compare (Sci s _ _) SciZ = case s of
                                  Positive => GT
                                  Negative => LT
  compare (Sci s c e) (Sci s' c' e') =
    case (s, s') of
         (Positive, Positive) => case compare e e' of
                                      EQ => compare c c'
                                      comp => comp
         (Positive, Negative) => GT
         (Negative, Positive) => LT
         (Negative, Negative) => case compare e' e of
                                      EQ => compare c' c
                                      comp => comp

infixl 9 ^
private
(^) : Nat -> Nat -> Nat
x ^ Z = 1
x ^ (S k) = x * (x ^ k)

private
digitsToNat : {b : _} -> List (Fin (S (S b))) -> Nat
digitsToNat [] = 0
digitsToNat (x::xs) = finToNat x + (S (S b)) * digitsToNat xs

export
toInteger : {b : _} -> Scientific b -> Maybe Integer
toInteger SciZ = Just 0
toInteger (Sci s c e) =
  if e >= 0
     then case c of
               CoeffInt x => Just $ withSign $ finToNat (FS x) * (b ^ integerToNat e)
               CoeffFloat x xs x' => let digits = reverse $ (FS x) :: xs ++ [FS x']
                                         e' = e - natToInteger (length (xs ++ [FS x']))
                                     in if e' >= 0
                                           then Just $ withSign $ digitsToNat digits * (b ^ integerToNat e')
                                           else Nothing
     else Nothing
where
  withSign : Nat -> Integer
  withSign = case s of
                  Negative => negate . natToInteger
                  Positive => natToInteger

export
negate : Scientific b -> Scientific b
negate SciZ = SciZ
negate (Sci s c e) = let s' = case s of
                                   Positive => Negative
                                   Negative => Positive
                     in Sci s' c e

export
abs : Scientific b -> Scientific b
abs SciZ = SciZ
abs (Sci _ c e) = Sci Positive c e

-- TODO: What happens, when Integer is negative? Low priority, since this is private.
||| The digits of an Integer, least significant first.
private
integerDigits : {b : _} -> Integer -> List (Fin (S (S b)))
integerDigits 0 = []
integerDigits x = d :: integerDigits r where
  d : Fin (S (S b))
  d = restrict (S b) x
  r : Integer
  r = x `div` natToInteger (S (S b))

||| Remove the zeros near the head of a list.
private
removeLeadingZeros : List (Fin (S (S b))) -> Maybe (Fin (S b), List (Fin (S (S b))))
removeLeadingZeros [] = Nothing
removeLeadingZeros (FZ :: xs) = removeLeadingZeros xs
removeLeadingZeros (FS x :: xs) = Just (x, xs)

private
fromDigits : List (Fin (S (S b))) -> Scientific (S (S b))
fromDigits ys =
  case removeLeadingZeros $ reverse ys of
       Nothing => SciZ
       Just (x, ys') => case removeLeadingZeros $ reverse ys' of
                            Nothing => Sci Positive (CoeffInt x) (cast $ length ys')
                            Just (x', xs) => Sci Positive (CoeffFloat x (reverse xs) x') (cast $ length ys')

export
fromFin : Fin (S (S b)) -> Scientific (S (S b))
fromFin FZ = SciZ
fromFin (FS x) = Sci Positive (CoeffInt x) 0

export
fromInteger : {b : _} -> Integer -> Scientific (S (S b))
fromInteger x = if x < 0
                   then negate $ fromIntegerPositive x
                   else fromIntegerPositive x
where
  fromIntegerPositive : Integer -> Scientific (S (S b))
  fromIntegerPositive = fromDigits . integerDigits . abs

export
fromNat : {b : _} -> Nat -> Scientific (S (S b))
fromNat = fromInteger . natToInteger

||| Single bit full adder in base (S (S b)).
private
plusBit : (op : Sign) ->
          {b : _} ->
          (carry : Bool) ->
          Fin (S (S b)) ->
          Fin (S (S b)) ->
          ((Fin (S (S b))), Bool)
plusBit op False x FZ = (x, False)
plusBit Positive True x FZ = case strengthen $ FS FZ of
                                  Nothing => (FZ, True)
                                  Just z => (z, False)
plusBit Negative True x FZ = case x of
                                  FZ => (last, True)
                                  FS z => (weaken z, False)
plusBit Positive carry x (FS y) = case strengthen $ FS x of
                                       Nothing => (fst $ plusBit Positive carry FZ (weaken y), True)
                                       Just z => plusBit Positive carry z (weaken y)
plusBit Negative carry x (FS y) = case x of
                                       FZ => (fst $ plusBit Negative carry last (weaken y), True)
                                       FS z => plusBit Negative carry (weaken z) (weaken y)

||| N bit full adder in base (S (S b)).
export
plusBits : (op : Sign) ->
           {b : _} ->
           (carry : Bool) ->
           Vect n (Fin (S (S b))) ->
           Vect n (Fin (S (S b))) ->
           (Vect n (Fin (S (S b))), Bool)
plusBits op carry [] [] = ([], carry)
plusBits op carry (x :: xs) (y :: ys) =
  let (z, carry') = plusBit op carry x y
      (zs, sign) = plusBits op carry' xs ys
  in (z :: zs, sign)

-- TODO: Add NonEmpty to result type.
||| All bits of a Coefficient, least significant first.
export
coefficientBits : Coefficient (S (S b)) -> List (Fin (S (S b)))
coefficientBits (CoeffInt x) = [FS x]
coefficientBits (CoeffFloat x xs x') = reverse $ FS x :: xs ++ [FS x']

-- TODO: get a definiton like this working:
--equalizeLength : a ->
--                 (xs : List a) ->
--                 (ys : List a) ->
--                 (Vect (max (length xs) (length ys)) a, Vect (max (length xs) (length ys)) a)
private
equalizeLength : a ->
                (n : _) ->
                (xs : List a) ->
                (ys : List a) ->
                (Vect n a, Vect n a)
equalizeLength a Z _ _ = ([],[])
equalizeLength a (S k) [] [] = let (ps, qs) = equalizeLength a k [] []
                               in (a :: ps, a :: qs)
equalizeLength a (S k) [] (y::ys) = let (ps, qs) = equalizeLength a k [] ys
                                    in (a :: ps, y :: qs)
equalizeLength a (S k) (x::xs) [] = let (ps, qs) = equalizeLength a k xs []
                                    in (x :: ps, a :: qs)
equalizeLength a (S k) (x::xs) (y::ys) = let (ps, qs) = equalizeLength a k xs ys
                                         in (x :: ps, y :: qs)

||| Wrapper for plusBits, adding padding regarding the exponent and trailing zeros.
private
plusBits' : (op : Sign) ->
            {b : _} ->
            (List (Fin (S (S b))), Integer) ->
            (List (Fin (S (S b))), Integer) ->
            (List (Fin (S (S b))), Bool)
plusBits' op (xs,xe) (ys,ye) =
  let n = max (length xs) (length ys)
      (xs'', ys'') = equalizeLength FZ n xs' ys'
      (zs, overflow) = plusBits op False (reverse xs'') (reverse ys'')
  in (toList zs, overflow) where
    xs' : List (Fin (S (S b)))
    xs' = reverse $ xs ++ replicate (integerToNat ye `minus` integerToNat xe) FZ
    ys' : List (Fin (S (S b)))
    ys' = reverse $ ys ++ replicate (integerToNat xe `minus` integerToNat ye) FZ

-- TODO: remove this or removeLeadingZeros
private
removeLeadingZeros' : List (Fin (S (S b))) -> (Nat, Maybe (Fin (S b), List (Fin (S (S b)))))
removeLeadingZeros' [] = (Z, Nothing)
removeLeadingZeros' (FZ :: xs) = let (n, res) = removeLeadingZeros' xs
                                 in (S n, res)
removeLeadingZeros' (FS x :: xs) = (Z, Just (x, xs))

||| Requires the digits to be ordered, least significant first.
||| Returns Coefficient and number of significant zeros.
private
fromDigits' : List (Fin (S (S b))) -> (Maybe (Coefficient (S (S b))), Nat)
fromDigits' ys =
  let (n, removedLeading) = removeLeadingZeros' $ reverse ys
  in case removedLeading of
          Nothing => (Nothing, n)
          Just (x, ys') => case removeLeadingZeros $ reverse ys' of
                               Nothing => (Just (CoeffInt x), n)
                               Just (x', xs) => (Just (CoeffFloat x (reverse xs) x'), n)

export
(+) : {b : _} -> Scientific (S (S b)) -> Scientific (S (S b)) -> Scientific (S (S b))
SciZ + y = y
x + SciZ = x
x@(Sci s c e) + y@(Sci s' c' e') =
  let (zs, bit) = plusBits' op (xs, e) (ys, e')
  in case op of
          Positive => let s'' = s
                          bits = if bit then [FS FZ] else [FZ]
                      in case fromDigits' $ zs ++ bits of
                              (Nothing, _) => SciZ
                              (Just c'', bitShift) => let e'' = max e e' + 1 - natToInteger bitShift
                                                      in Sci s'' c'' e''
          Negative => let s'' = if bit then s' else s
                      in case fromDigits' zs of
                              (Nothing, _) => SciZ
                              (Just c'', bitShift) => let e'' = max e e' - natToInteger bitShift
                                                      in Sci s'' c'' e''
where
  op : Sign
  op = if s == s'
          then Positive
          else Negative
  xs : List (Fin (S (S b)))
  xs = coefficientBits c
  ys : List (Fin (S (S b)))
  ys = coefficientBits c'

(-) : {b : _} -> Scientific (S (S b)) -> Scientific (S (S b)) -> Scientific (S (S b))
x - y = x + negate y

-- TODO
||| Multiply two Coefficients and return True in the Bool, when the product is greater than the base.
private
multCoefficents : {b : _} -> Coefficient (S (S b)) -> Coefficient (S (S b)) -> (Coefficient (S (S b)), Bool)
multCoefficents (CoeffInt x) (CoeffInt y) =
  case integerToFin res (S b) of
       Nothing => (CoeffInt $ restrict b res, True)
       Just fin => (CoeffInt fin, False)
where
  res : Integer
  res = (finToInteger x + 1) * (finToInteger y + 1) - 1
multCoefficents a@(CoeffInt x) b@(CoeffFloat y ys y') = multCoefficents b a
-- TODO: finish multCoefficents
multCoefficents (CoeffFloat x xs x') (CoeffInt y) = ?multCoefficents_rhs_2
multCoefficents (CoeffFloat x xs x') (CoeffFloat y ys y') = ?multCoefficents_rhs_3

export
(*) : {b : _} -> Scientific (S (S b)) -> Scientific (S (S b)) -> Scientific (S (S b))
SciZ * y = SciZ
x * SciZ = SciZ
(Sci s c e) * (Sci s' c' e') = Sci s'' c'' e'' where
  coefficientPair : (Coefficient (S (S b)), Bool)
  coefficientPair = multCoefficents c c'
  s'' : Sign
  s'' = if s == s'
           then Positive
           else Negative
  c'' : Coefficient (S (S b))
  c'' = fst coefficientPair
  e'' : Integer
  e'' = if snd coefficientPair
           then e + e' + 1
           else e + e'

-- -- TODO: implementations don't work because the base (S (S b)) isn't accessible in the method's context.
-- -- TODO: consider other implementations:
-- -- - Fractional might not terminate, because of infinite representation
-- -- - Integral doesn't sound like it would fit, but mod and div make still make sense
-- public export
-- Num (Scientific b) where
--   -- (+) = (+)
--   -- (*) = (*)
--   -- fromInteger = fromInteger

-- public export
-- Neg (Scientific b) where
--   -- negate = negate
--   -- (-) = (-)

-- public export
-- Abs (Scientific b) where
--   -- abs = abs

||| Create string representing using scientific notation.
export
prettyShowScientific : Scientific 10 -> String
prettyShowScientific SciZ = "0"
prettyShowScientific (Sci s c e) = prettyShowSign s ++ prettyShowCoefficient c ++ prettyExponent where
  prettyExponent : String
  prettyExponent = case e of
                        0 => ""
                        x => "e" ++ show x


text:
module Sub02Apply54x12

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(18x+4) --A[6,-4]->E[2,-4]--> 3(2x)
export
apply54x12 : (Not . P) (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                            (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))))
  -> (m : Nat **
        (LTE (S m)
             (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                               (S (plus (plus (plus l l) l)
                                        (plus (plus l l) l))))
                         (S (plus (plus (plus l l) l) (plus (plus l l) l)))))),
         (Not . P) m))
apply54x12 {l} col = ((plus l l) ** (lte54x12 l, ae54x12To6x l col)) where
  lte54x12 : (l:Nat) -> LTE (S (plus l l))
                            (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                  (S (plus (plus (plus l l) l)
                                           (plus (plus l l) l))))
                            (S (plus (plus (plus l l) l)
                                     (plus (plus l l) l))))))
  lte54x12 Z = LTESucc LTEZero
  lte54x12 (S k) = let lemma = lte54x12 k in rewrite (sym (plusSuccRightSucc k k)) in
    rewrite (sym (plusSuccRightSucc (plus k k) k)) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (plus (plus k k) k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (plus (plus k k) k)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (plus (plus k k) k))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (plus (plus k k) k)) (S (S (S (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (plus (plus k k) k)) (S (S (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (plus (plus k k) k)) (S (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (plus (plus k k) k)) (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (plus (plus k k) k)) (S (S (plus (plus (plus k k) k) (plus (plus k k) k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k)))) (S (S (S (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k)))) (S (S (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k)))) (S (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (plus (plus k k) k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k)))) (S (S (plus (plus (plus k k) k) (plus (plus k k) k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (plus (plus k k) k)) (S (plus (plus (plus k k) k) (plus (plus k k) k)))) (S (plus (plus (plus k k) k) (plus (plus k k) k))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc) lemma


text:
import Data.So
import Data.Vect

--------------------------------------------------------------------------------
-- Utility

-- Makes a best effort to return an error message.
-- Use this only on code paths that you can deduce should be unreachable.
unsafeError : String -> a
unsafeError message = believe_me message

-- Unwraps a `Just a` to a plain `a`.
-- Useful for command-line debugging but unsafe for general program usage.
unsafeUnwrapJust : (Maybe a) -> a
unsafeUnwrapJust (Just x) =
    x
unsafeUnwrapJust (Nothing) =
    unsafeError "The specified Maybe was not a Just."

--------------------------------------------------------------------------------
-- IsLte

-- Proof that `x <= y`.
IsLte : Ord e => (x:e) -> (y:e) -> Type
IsLte x y = So (x <= y)

mkIsLte : Ord e => (x:e) -> (y:e) -> Maybe (IsLte x y)
mkIsLte x y =
    case choose (x <= y) of
        Left proofXLteY =>
            Just proofXLteY
        Right proofNotXLteY =>
            Nothing

-- Given an `x` and a `y`, returns a proof that either `x <= y` or `y <= x`.
chooseLte :
    Ord e =>
    (x:e) -> (y:e) ->
    Either (IsLte x y) (IsLte y x)
chooseLte x y =
    case choose (x <= y) of
        Left proofXLteY =>
            Left proofXLteY
        Right proofNotXLteY =>
            -- Given: not (x <= y)
            -- Derive: x > y
            -- Derive: y < x
            -- Derive: y <= x
            --
            -- Unfortunately Ord doesn't guarantee the preceding
            -- even though any sane implementation will conform
            -- to those rules.
            case choose (y <= x) of
                Left proofYLteX =>
                    Right proofYLteX
                Right proofNotYLteX =>
                    unsafeError "Impossible with a sane Ord implementation."

--------------------------------------------------------------------------------
-- IsSorted

-- Proof that `xs` is sorted.
data IsSorted : (xs:Vect n e) -> Type where
    IsSortedZero :
        IsSorted Nil
    IsSortedOne  :
        Ord e =>
        (x:e) ->
        IsSorted (x::Nil)
    IsSortedMany :
        Ord e =>
        (x:e) -> (y:e) -> (ys:Vect n'' e) ->    -- (n'' == (n - 2))
        (IsLte x y) -> IsSorted (y::ys) ->
        IsSorted (x::(y::ys))

mkIsSorted : Ord e => (xs:Vect n e) -> Maybe (IsSorted xs)
mkIsSorted Nil =
    Just IsSortedZero
mkIsSorted (x::Nil) =
    Just (IsSortedOne x)
mkIsSorted (x::(y::ys)) =
    case (mkIsLte x y) of
        Just proofXLteY =>
            case (mkIsSorted (y::ys)) of
                Just proofYYsIsSorted =>
                    Just (IsSortedMany x y ys proofXLteY proofYYsIsSorted)
                Nothing =>
                    Nothing
        Nothing =>
            Nothing

--------------------------------------------------------------------------------
-- ElemsAreSame

-- Proof that set `xs` and set `ys` contain the same elements.
data ElemsAreSame : (xs:Vect n e) -> (ys:Vect n e) -> Type where
    NilIsNil :
        ElemsAreSame Nil Nil
    PrependXIsPrependX :
        (x:e) -> ElemsAreSame zs zs' ->
        ElemsAreSame (x::zs) (x::zs')
    PrependXYIsPrependYX :
        (x:e) -> (y:e) -> ElemsAreSame zs zs' ->
        ElemsAreSame (x::(y::zs)) (y::(x::(zs')))
    -- NOTE: Probably could derive this last axiom from the prior ones
    SamenessIsTransitive :
        ElemsAreSame xs zs -> ElemsAreSame zs ys ->
        ElemsAreSame xs ys

XsIsXs : (xs:Vect n e) -> ElemsAreSame xs xs
XsIsXs Nil =
    NilIsNil
XsIsXs (x::ys) =
    PrependXIsPrependX x (XsIsXs ys)

flip : ElemsAreSame xs ys -> ElemsAreSame ys xs
flip NilIsNil =
    NilIsNil
flip (PrependXIsPrependX x proofXsTailIsYsTail) =
    PrependXIsPrependX x (flip proofXsTailIsYsTail)
flip (PrependXYIsPrependYX x y proofXsLongtailIsYsLongtail) =
    PrependXYIsPrependYX y x (flip proofXsLongtailIsYsLongtail)
flip (SamenessIsTransitive proofXsIsZs proofZsIsYs) =
    let proofYsIsZs = flip proofZsIsYs in
    let proofZsIsXs = flip proofXsIsZs in
    let proofYsIsXs = SamenessIsTransitive proofYsIsZs proofZsIsXs in
    proofYsIsXs

-- NOTE: Needed to explicitly pull out the {x}, {y}, {zs}, {us} implicit parameters.
swapFirstAndSecondOfLeft : ElemsAreSame (x::(y::zs)) us -> ElemsAreSame (y::(x::zs)) us
swapFirstAndSecondOfLeft {x} {y} {zs} {us} proofXYZsIsUs =
    let proofYXZsIsXYZs = PrependXYIsPrependYX y x (XsIsXs zs) in
    let proofYZZsIsUs = SamenessIsTransitive proofYXZsIsXYZs proofXYZsIsUs in
    proofYZZsIsUs

--------------------------------------------------------------------------------
-- HeadIs, HeadIsEither

-- Proof that the specified vector has the specified head.
data HeadIs : Vect n e -> e -> Type where
    MkHeadIs : HeadIs (x::xs) x

-- Proof that the specified vector has one of the two specified heads.
--
-- NOTE: Could implement this as an `Either (HeadIs xs x) (HeadIs xs y)`,
--       but an explicit formulation feels cleaner.
data HeadIsEither : Vect n e -> (x:e) -> (y:e) -> Type where
    HeadIsLeft  : HeadIsEither (x::xs) x y
    HeadIsRight : HeadIsEither (x::xs) y x

--------------------------------------------------------------------------------
-- Insertion Sort

-- Inserts an element into a non-empty sorted vector, returning a new
-- sorted vector containing the new element plus the original elements.
insert' :
    Ord e =>
    (xs:Vect (S n) e) -> (y:e) -> (IsSorted xs) -> (HeadIs xs x) ->
    (xs':(Vect (S (S n)) e) ** ((IsSorted xs'), (HeadIsEither xs' x y), (ElemsAreSame (y::xs) xs')))
insert' (x::Nil) y (IsSortedOne x) MkHeadIs =
    case (chooseLte x y) of
        Left proofXLteY =>
            let yXNilSameXYNil = PrependXYIsPrependYX y x (XsIsXs Nil) in
            (x::(y::Nil) **
             (IsSortedMany x y Nil proofXLteY (IsSortedOne y),
              HeadIsLeft,
              yXNilSameXYNil))
        Right proofYLteX =>
            let yXNilSameYXNil = XsIsXs (y::(x::Nil)) in
            (y::(x::Nil) **
             (IsSortedMany y x Nil proofYLteX (IsSortedOne x),
              HeadIsRight,
              yXNilSameYXNil))
insert' (x::(y::ys)) z proofXYYsIsSorted MkHeadIs =
    case proofXYYsIsSorted of
        (IsSortedMany x y ys proofXLteY proofYYsIsSorted) =>
            case (chooseLte x z) of
                Left proofXLteZ =>
                    -- x::(insert' (y::ys) z)
                    let proofHeadYYsIsY = the (HeadIs (y::ys) y) MkHeadIs in
                    case (insert' (y::ys) z proofYYsIsSorted proofHeadYYsIsY) of
                        -- rest == (_::tailOfRest)
                        ((y::tailOfRest) ** (proofRestIsSorted, HeadIsLeft, proofZYYsSameRest)) =>
                            let proofXZYYsIsXRest = PrependXIsPrependX x proofZYYsSameRest in
                            let proofZXYYsIsXRest = swapFirstAndSecondOfLeft proofXZYYsIsXRest in
                            (x::(y::tailOfRest) **
                             (IsSortedMany x y tailOfRest proofXLteY proofRestIsSorted,
                              HeadIsLeft,
                              proofZXYYsIsXRest))
                        ((z::tailOfRest) ** (proofRestIsSorted, HeadIsRight, proofZYYsSameRest)) =>
                            let proofXZYYsIsXRest = PrependXIsPrependX x proofZYYsSameRest in
                            let proofZXYYsIsXRest = swapFirstAndSecondOfLeft proofXZYYsIsXRest in
                            (x::(z::tailOfRest) **
                             (IsSortedMany x z tailOfRest proofXLteZ proofRestIsSorted,
                              HeadIsLeft,
                              proofZXYYsIsXRest))
                Right proofZLteX =>
                    -- z::(x::(y::ys))
                    let proofZXYYsIsZXYYs = XsIsXs (z::(x::(y::ys))) in
                    (z::(x::(y::ys)) **
                     (IsSortedMany z x (y::ys) proofZLteX proofXYYsIsSorted,
                      HeadIsRight,
                      proofZXYYsIsZXYYs))

-- Inserts an element into a sorted vector, returning a new
-- sorted vector containing the new element plus the original elements.
insert :
    Ord e =>
    (xs:Vect n e) -> (y:e) -> (IsSorted xs) ->
    (xs':(Vect (S n) e) ** ((IsSorted xs'), (ElemsAreSame (y::xs) xs')))
insert Nil y IsSortedZero =
    ([y] ** (IsSortedOne y, XsIsXs [y]))
insert (x::xs) y proofXXsIsSorted =
    let proofHeadOfXXsIsX = the (HeadIs (x::xs) x) MkHeadIs in
    case (insert' (x::xs) y proofXXsIsSorted proofHeadOfXXsIsX) of
        (xs' ** (proofXsNewIsSorted, proofHeadXsNewIsXOrY, proofYXXsIsXsNew)) =>
            (xs' ** (proofXsNewIsSorted, proofYXXsIsXsNew))

-- Sorts the specified vector,
-- returning a new sorted vector with the same elements.
insertionSort :
    Ord e =>
    (xs:Vect n e) ->
    (xs':Vect n e ** (IsSorted xs', ElemsAreSame xs xs'))
insertionSort Nil =
    (Nil ** (IsSortedZero, NilIsNil))
insertionSort (x::ys) =
    case (insertionSort ys) of
        (ysNew ** (proofYsNewIsSorted, proofYsIsYsNew)) =>
            case (insert ysNew x proofYsNewIsSorted) of
                (result ** (proofResultIsSorted, proofXYsNewIsResult)) =>
                    let proofXYsIsXYsNew = PrependXIsPrependX x proofYsIsYsNew in
                    let proofXYsIsResult = SamenessIsTransitive proofXYsIsXYsNew proofXYsNewIsResult in
                    (result ** (proofResultIsSorted, proofXYsIsResult))

--------------------------------------------------------------------------------
-- Main

-- Parses an integer from a string, returning 0 if there is an error.
parseInt : String -> Integer
parseInt s =
    the Integer (cast s)

-- Joins a list of elements with the provided separator,
-- returning a separator-separated string.
intercalate : Show e => (xs:Vect n e) -> (sep:String) -> String
intercalate Nil sep =
    ""
intercalate (x::Nil) sep =
    show x
intercalate (x::(y::zs)) sep =
    (show x) ++ sep ++ (intercalate (y::zs) sep)

main : IO ()
main = do
    putStrLn "Please type a space-separated list of integers: "
    csv <- getLine
    let numbers = map parseInt (words csv)
    let (sortedNumbers ** (_, _)) = insertionSort (fromList numbers)
    putStrLn "After sorting, the integers are: "
    putStrLn (intercalate sortedNumbers " ")

--------------------------------------------------------------------------------

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Main

import IdrisJvm.FFI
import IdrisJvm.IO
import Java.Lang
import Java.Util
import Java.Math
import Java.Util.Function
import Java.Util.Stream
import Data.Vect

term syntax "<@TestAnn>" [attrs] = <@> "idrisjvm/integrationtest/TestAnn" attrs
term syntax "<@TestAnn2>" [attrs] = <@> "idrisjvm/integrationtest/TestAnn2" attrs

term syntax "<@TimeUnit>" [timeUnit] = <@enum> "java/util/concurrent/TimeUnit" timeUnit

IdrisThreadClass : JVM_NativeTy
IdrisThreadClass = Class "hello/IdrisThread"

IdrisThread : Type
IdrisThread = JVM_Native IdrisThreadClass

add : IdrisThread -> Int -> Int -> Int
add _ x y = x + y

exportedBoolToString : Bool -> String
exportedBoolToString = show

helloFromIdris' : IdrisThread -> String -> JVM_IO String
helloFromIdris' this name = do
  printLn "Hi "
  pure $ "Hello " ++ name

helloFromIdris : IdrisThread -> String -> JVM_IO String
helloFromIdris this name = helloFromIdris' this name

Inherits Thread IdrisThread where {}

setName : IdrisThread -> String -> JVM_IO ()
setName this name = invokeInstance "setName" (IdrisThread -> String -> JVM_IO ()) this name

getThreadName : IdrisThread -> JVM_IO String
getThreadName = invokeInstance "getThreadName" (IdrisThread -> JVM_IO String)

run' : IdrisThread -> JVM_IO ()
run' this = do
  threadName <- getThreadName this
  printLn !(helloFromIdris this threadName)

run : IdrisThread -> JVM_IO ()
run this = run' this

jmain : JVM_Array String -> JVM_IO ()
jmain args = do
  printLn $ exportedBoolToString True
  Arrays.toString args >>= printLn

idrisThreadConstructor : IdrisThread -> JVM_IO ()
idrisThreadConstructor thread = printLn "hello from constructor"

idrisThreadWithNameConstructor : IdrisThread -> String -> JVM_IO ()
idrisThreadWithNameConstructor thread name = printLn $ "hello from constructor with name: " ++ name

newIdrisThread : JVM_IO IdrisThread
newIdrisThread = FFI.new (JVM_IO IdrisThread)

newIdrisThreadWithName : String -> JVM_IO IdrisThread
newIdrisThreadWithName = FFI.new (String -> JVM_IO IdrisThread)

startIdrisThread : IdrisThread -> JVM_IO ()
startIdrisThread thread = invokeInstance "start" (IdrisThread -> JVM_IO ()) thread

jadd : IdrisThread -> Int -> Int -> Int
jadd thread x y = unsafePerformIO $ invokeInstance "jadd" (IdrisThread -> Int -> Int -> JVM_IO Int) thread x y

jboolToString : Bool -> String
jboolToString b = unsafePerformIO $ invokeStatic IdrisThreadClass "boolToString" (Bool -> JVM_IO String) b

jhelloFromIdris : IdrisThread -> String -> JVM_IO String
jhelloFromIdris thread str = invokeInstance "helloFromIdris" (IdrisThread -> String -> JVM_IO String) thread str

emptyList : List Int
emptyList = []

cons : Int -> List Int -> List Int
cons x xs = x :: xs

append : List Int -> List Int -> List Int
append xs ys = xs ++ ys

showList : List Int -> String
showList = show

ListIntClass : JVM_NativeTy
ListIntClass = Class "hello/ListInt"

ListInt : Type
ListInt = JVM_Native ListIntClass

JExportTestClass : JVM_NativeTy
JExportTestClass = Class "hello/JExportTest"

JExportTest : Type
JExportTest = JVM_Native JExportTestClass

jappend : ListInt -> ListInt -> ListInt
jappend xs ys = unsafePerformIO $ invokeStatic JExportTestClass "append" (ListInt -> ListInt -> JVM_IO ListInt) xs ys

jcons : Int -> ListInt -> ListInt
jcons x xs = unsafePerformIO $ invokeStatic JExportTestClass "cons" (Int -> ListInt -> JVM_IO ListInt) x xs

jemptyList : ListInt
jemptyList = unsafePerformIO $ invokeStatic JExportTestClass "emptyList" (JVM_IO ListInt)

jshowList : ListInt -> String
jshowList xs = unsafePerformIO $ invokeStatic JExportTestClass "showList" (ListInt -> JVM_IO String) xs

joneToTen : ListInt
joneToTen = unsafePerformIO $ invokeStatic JExportTestClass "oneToTen" (JVM_IO ListInt)

Show ListInt where
  show = jshowList

setNumbers : IdrisThread -> ListInt -> JVM_IO ()
setNumbers thread nums = setInstanceField "numbers" (IdrisThread -> ListInt ->  JVM_IO ()) thread nums

getNumbers : IdrisThread -> JVM_IO (ListInt)
getNumbers = getInstanceField "numbers" (IdrisThread -> JVM_IO (ListInt))

setStaticNumbers : ListInt -> JVM_IO ()
setStaticNumbers nums = setStaticField IdrisThreadClass "numbersStatic" (ListInt ->  JVM_IO ()) nums

getStaticNumbers : JVM_IO (ListInt)
getStaticNumbers = getStaticField IdrisThreadClass "numbersStatic" (JVM_IO (ListInt))

oneToTen : List Int
oneToTen = [1..10]

-- currently only null is allowed for field initialization but the value can be set later using `setInstanceField`
-- and `setStaticField` functions. See above for the usage of those functions.
numbersField : List Int
numbersField = believe_me prim__null

-- To test passing nulls to Java using Maybe
nullableToString : Inherits Object that => Maybe that -> String
nullableToString obj = unsafePerformIO $ invokeStatic ObjectsClass "toString" (Object -> JVM_IO String) (maybeToNullable $ believe_me obj)

-- To test passing null to Java for String using Maybe
equalsIgnoreCase : String -> Maybe String -> Bool
equalsIgnoreCase str1 str2 = unsafePerformIO $ invokeInstance "equalsIgnoreCase" (String -> String -> JVM_IO Bool) str1 (maybeToNullableString str2)

getName : JClass -> String
getName clazz = unsafePerformIO $ invokeInstance "getName" (JClass -> JVM_IO String) clazz

stringClassLit : JClass
stringClassLit = classLit "java/lang/String"

intClassLit : JClass
intClassLit = classLit "int"

booleanClassLit : JClass
booleanClassLit = classLit "boolean"

byteClassLit : JClass
byteClassLit = classLit "byte"

charClassLit : JClass
charClassLit = classLit "char"

shortClassLit : JClass
shortClassLit = classLit "short"

longClassLit : JClass
longClassLit = classLit "long"

floatClassLit : JClass
floatClassLit = classLit "float"

doubleClassLit : JClass
doubleClassLit = classLit "double"

lambdaTest1 : JVM_IO ()
lambdaTest1 = ArrayList.fromList ["foobar", "hello", "world"] >>=
              stream >>=
              filter (jlambda (not . isPrefixOf "foo")) >>=
              map (jlambda Strings.reverse) >>=
              collect !toList >>=
              Objects.toString >>=
              printLn

lambdaTest2 : JVM_IO ()
lambdaTest2 = do
  let runnable = (jlambda $ printLn "hello")
  Runnable.run runnable

lambdaTest3 : JVM_IO ()
lambdaTest3 = generate (Supplier.jlambda (pure "hello")) >>=
              limit 3 >>=
              collect !toList >>=
              Objects.toString >>=
              printLn

lambdaTest4 : JVM_IO ()
lambdaTest4 = IntStream.from !(vectToArray [2, 4, 6]) >>=
              map (jlambda (+1)) >>=
              sum >>=
              printLn

main : JVM_IO ()
main = do
  -- Test ffi calls
  printLn $ maxInt 3 5
  printLn $ maxFloat (Float 3.2) (Float 5.5)
  printLn $ maxDouble 7.5 6.8
  printLn $ boolToString $ parseBool "true"
  printLn $ charToString $ charAt "foobarbaz" 3
  printLn $ byteToString $ parseByte "127"
  printLn $ shortToString $ parseShort "32767"
  printLn $ longToString $ parseLong "9223372036854775807"

  printLn !(getProperty "foo")  -- Test returning null string from FFI call
  System.setProperty "foo" "fooval"
  printLn !(getProperty "foo")  -- Test returning a non-null string from FFI call
  hashMap <- HashMap.new
  putStrLn $ !(maybe (pure "null") (Objects.toString) !(HashMap.get hashMap "bar"))-- Test returning null object
  HashMap.put hashMap (Just "bar") (Just "barval")
  putStrLn $ !(maybe (pure "null") (Objects.toString) !(HashMap.get hashMap "bar")) -- Test returning a non-null object

  printLn $ nullableToString (the (Maybe BigInteger) Nothing) -- Test passing Nothing as a null to FFI call
  bigOne <- BigInteger.new "1"
  printLn $ nullableToString (Just bigOne) -- Test passing a `Just` as a non null value to FFI call
  printLn $ equalsIgnoreCase "foo" (Just "foo") -- Test passing a `Just` as a non null String to FFI call
  printLn $ equalsIgnoreCase "foo" (the (Maybe String) Nothing) -- Test passing nothing as a null String to FFI call
  bigInt1 <- BigInteger.new "11111111111111111111"
  bigInt2 <- BigInteger.new "11111111111111111111"
  printLn $ BigInteger.toString $ BigInteger.add bigInt1 bigInt2
  jlist <- ArrayList.new
  printLn !(size jlist)
  -- Test exports
  thread1 <- newIdrisThread
  setName thread1 "idris-thread"
  startIdrisThread thread1
  printLn $ Main.add thread1 2 3
  printLn $ jadd thread1 3 5
  printLn $ jboolToString True
  printLn $ !(jhelloFromIdris thread1 "from idris")

  thread2 <- newIdrisThreadWithName "idris-thread-2"
  startIdrisThread thread2

  printLn $ jshowList $ jappend (jcons 3 (jcons 4 jemptyList)) (jcons 5 (jcons 6 jemptyList))

  setNumbers thread1 joneToTen  -- Test setting an instance field
  printLn !(getNumbers thread1) -- Test getting an instance field

  setStaticNumbers joneToTen -- Test setting a static field
  printLn !getStaticNumbers -- Test getting a static field

  printLn $ getName <$> the (List JClass) [ stringClassLit, intClassLit, byteClassLit, charClassLit, shortClassLit,
                            booleanClassLit, longClassLit, floatClassLit, doubleClassLit ]

  lambdaTest1
  lambdaTest2
  lambdaTest3
  lambdaTest4

exports1 : FFI_Export FFI_JVM "hello/IdrisThread extends java/lang/Thread implements java/lang/Runnable" []
exports1 =
  Data (List Int) "hello/ListInt" $
  Fun numbersField (ExportInstanceField "numbers") $
  Fun numbersField (ExportStaticField "numbersStatic") $
  Fun exportedBoolToString (ExportStatic "boolToString") $
  Fun Main.add (ExportInstance "jadd") $
  Fun helloFromIdris ExportDefault $
  Fun idrisThreadConstructor Constructor $
  Fun idrisThreadWithNameConstructor Constructor $
  Fun Main.run ExportDefault $
  Fun getThreadName (Super "getName") $
  Fun Main.jmain (ExportStatic "main") $
  Fun helloFromIdris (ExportStaticWithAnn "helloWithAnnotation"
      -- method annotations
      [
        -- method annotation 1
        <@TestAnn> [
          ("intValue", <@i> "5"),
          ("byteValue", <@by> "5"),
          ("charValue", <@ch> "a"),
          ("booleanValue", <@b> "false"),
          ("shortValue", <@sh> "45"),
          ("longValue", <@l> "2324"),
          ("floatValue", <@f> "1.32"),
          ("doubleValue", <@d> "4.2323"),
          ("enumValue", <@TimeUnit> "SECONDS"),
          ("annValue", <@@> <@TestAnn2> [
              ("shortValue", <@sh> "45")
              ]),
          ("annValues", <@..> [
              <@@> <@TestAnn2> [
                  ("shortValue", <@sh> "45"),
                  ("classValue", <@c> "int[][]")
                  ],
              <@@> <@TestAnn2> [
                  ("enumValue", <@TimeUnit> "MILLISECONDS")
                  ]
              ])
        ],

        -- method annotation 2
        <@TestAnn2> []
      ]

      [
        -- parameter 1 annotations
        [
            -- parameter 1 - annotation 1
            <@TestAnn> [
                  ("doubleValue", <@d> "4.2323"),
                  ("enumValue", <@TimeUnit> "SECONDS"),
                  ("annValue", <@@> <@TestAnn2> [
                      ("shortValue", <@sh> "45")
                      ]),
                  ("annValues", <@..> [
                      <@@> <@TestAnn2> [
                          ("shortValue", <@sh> "45")
                          ],
                      <@@> <@TestAnn2> [
                          ("enumValue", <@TimeUnit> "MILLISECONDS")
                          ]
                      ])
                  ],
            -- parameter 1 - annotation 2
            <@TestAnn2> []
        ],

        -- parameter 2 annotations
        [<@TestAnn2> []]
      ])
  End

exports2 : FFI_Export FFI_JVM "hello/JExportTest" []
exports2 =
  Data (List Int) "hello/ListInt" $
  Fun cons (ExportStatic "cons") $
  Fun emptyList (ExportStatic "emptyList") $
  Fun showList (ExportStatic "showList") $
  Fun append (ExportStatic "append") $
  Fun oneToTen (ExportStatic "oneToTen") $
  End


text:
||| mutable queue
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Mutable.Queue

import Data.Container.Mutable.Array
import public Data.Container.Mutable.Interfaces

import Data.Fin
import Data.List
import Data.IORef
import System.Info
import Data.So

%default total

-- --------------------------------------------------------------------------
-- Backend specific mutable queue

namespace Prim

  data PrimIOQueue : Type -> Type where [external]

  %foreign "javascript:lambda:() => new Array()"
  prim__ioqueue_new : PrimIO (PrimIOQueue t)

  %foreign "javascript:lambda:(x, xs) => xs.push(x)"
  prim__ioqueue_push : t -> PrimIOQueue t -> PrimIO ()

  %foreign "javascript:lambda:(d, f, xs) => { const x = xs.shift(); return (x === undefined)? d : f(x); }"
  prim__ioqueue_pull : a -> (t -> a) -> PrimIOQueue t -> PrimIO a

  %foreign "javascript:lambda:(xs) => xs.length == 0"
  prim__ioqueue_null : PrimIOQueue t -> PrimIO Bool

  %foreign "javascript:lambda:(xs) => xs.length"
  prim__ioqueue_length : PrimIOQueue t -> PrimIO Int

  %inline export newPrimIOQueue : HasIO io => io (PrimIOQueue t)
  newPrimIOQueue = primIO $ prim__ioqueue_new

  export null : HasIO io => PrimIOQueue a -> io Bool
  null xs   = primIO $ prim__ioqueue_null xs

  export length : HasIO io => PrimIOQueue a -> io Nat
  length xs  = (primIO $ prim__ioqueue_length xs) >>= pure . fromInteger . cast

  export push : HasIO io => a -> PrimIOQueue a -> io Bool
  push x xs = (primIO $ prim__ioqueue_push x xs) >> pure True

  export pull : HasIO io => PrimIOQueue a -> io (Maybe a)
  pull xs   = primIO $ prim__ioqueue_pull Nothing Just xs

{-
  export
  HasIO io => MutableQueue io PrimIOQueue where
    null xs   = primIO $ prim__ioqueue_null xs
    length xs  = (primIO $ prim__ioqueue_length xs) >>= pure . fromInteger . cast
    push x xs = (primIO $ prim__ioqueue_push x xs) >> pure True
    pull xs   = primIO $ prim__ioqueue_pull Nothing Just xs
 -}

-- --------------------------------------------------------------------------

%inline public export
hasNativeIOQueue : Bool
hasNativeIOQueue with (codegen)
  hasNativeIOQueue | "javascript" = True
  hasNativeIOQueue | _            = False

-- --------------------------------------------------------------------------
-- Generic IOArray based mutable queue

namespace Generic

  record Bin t where
    constructor MkBin
    content : IOArray (Maybe t)
    link: IORef (Maybe $ Bin t)

  %inline InitialBinSize : Nat
  InitialBinSize = 511

  export
  record IOArrayQueue t where
    constructor MkIOArrayQueue
    allocsize : IORef Nat
    content : IORef (Nat, Nat, Bin t, Nat, Bin t)

  export newIOArrayQueue : HasIO io => io (IOArrayQueue t)
  newIOArrayQueue = do
    bin <- pure $ MkBin !(newIOArray (S InitialBinSize) Nothing) !(newIORef Nothing)
    pure $ MkIOArrayQueue !(newIORef InitialBinSize)
                        !(newIORef (0, 0, bin, 0, bin))

  export null : HasIO io => IOArrayQueue t -> io Bool
  null q   = readIORef q.content >>= pure . (0 ==) . fst

  export length : HasIO io => IOArrayQueue a -> io Nat
  length q  = readIORef q.content >>= pure . fst

  export push : HasIO io => a -> IOArrayQueue a -> io Bool
  push x q = do
    (c, n, b0, m, b1) <- readIORef q.content
    case natToFin n (S $ ubound b0.content) of
      Just n' => do
        writeIOArray b0.content n' (Just x)
        writeIORef q.content (S c, S n, b0, m, b1)
      Nothing => do
        l <- readIORef q.allocsize
        b2 <- pure $ MkBin !(newIOArray (S l) Nothing) !(newIORef Nothing)
        writeIORef b0.link (Just b2)
        writeIOArray b2.content 0 (Just x)
        writeIORef q.content (S c, 1, b2, m, b1)
    pure True

  export pull : HasIO io => IOArrayQueue a -> io (Maybe a)
  pull q = do
    ((S c), n, b0, m, b1) <- readIORef q.content
      | (Z, _, _, _, _) => pure Nothing
    if c == 0
       then writeIORef q.content (0, 0, b0, 0, b0)
       else if m == ubound b1.content
               then do
                 Just b2 <- readIORef b1.link
                   | Nothing => writeIORef q.content (0, 0, b0, 0, b0) -- never happens
                 writeIORef q.content (c, n, b0, 0, b2)
               else
                 writeIORef q.content (c, n, b0, m + 1, b1)
    let m' = restrict b1.content $ cast m
    r <- readIOArray b1.content m' -- always Just
    writeIOArray b1.content m' Nothing
    pure r

{-
export
HasIO io => MutableQueue io IOArrayQueue where
  null q   = readIORef q.content >>= pure . (0 ==) . fst
  length q  = readIORef q.content >>= pure . fst

  push x q = do
    (c, n, b0, m, b1) <- readIORef q.content
    case natToFin n (S $ ubound b0.content) of
      Just n' => do
        writeIOArray b0.content n' (Just x)
        writeIORef q.content (S c, S n, b0, m, b1)
      Nothing => do
        l <- readIORef q.allocsize
        b2 <- pure $ MkBin !(newIOArray (S l) Nothing) !(newIORef Nothing)
        writeIORef b0.link (Just b2)
        writeIOArray b2.content 0 (Just x)
        writeIORef q.content (S c, 1, b2, m, b1)
    pure True

  pull q = do
    ((S c), n, b0, m, b1) <- readIORef q.content
      | (Z, _, _, _, _) => pure Nothing
    if c == 0
       then writeIORef q.content (0, 0, b0, 0, b0)
       else if m == ubound b1.content
               then do
                 Just b2 <- readIORef b1.link
                   | Nothing => writeIORef q.content (0, 0, b0, 0, b0) -- never happens
                 writeIORef q.content (c, n, b0, 0, b2)
               else
                 writeIORef q.content (c, n, b0, m + 1, b1)
    let m' = restrict b1.content $ cast m
    r <- readIOArray b1.content m' -- always Just
    writeIOArray b1.content m' Nothing
    pure r
    -}

-- --------------------------------------------------------------------------

{-
%inline public export IOQueue : Type -> Type
IOQueue t  with (hasNativeIOQueue)
  IOQueue t | True  = PrimIOQueue t
  IOQueue t | False = IOArrayQueue t

%inline public export newIOQueue : HasIO io => io (IOQueue t)
newIOQueue with (hasNativeIOQueue)
  newIOQueue | True  = newPrimIOQueue
  newIOQueue | False = newIOArrayQueue
  -}
-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
||| Automatic deriviation of JSON conversion interfaces.
|||
||| (C) The Idris Community, 2021
module Language.LSP.Message.Derive

-- NOTE: Elaborator functions are evaluated as if they are defined inside the
-- call location module, thus imported functions used inside elaborator
-- functions should be exported publicly or explicitly imported at call
-- location.
import public Data.Maybe
import public Data.SortedMap
import Data.String
import Language.JSON
import public Language.JSON.Interfaces
import Language.Reflection

%language ElabReflection
%default total

||| Options for automatic derivation of `ToJSON`/`FromJSON` instances.
public export
record JSONDeriveOpts where
  constructor MkOpts
  ||| If tagged, values are converted to JSON object with one field where the
  ||| key is the name of the constructor and the value is the object obtained
  ||| from converting the arguments of the constructor.
  tagged : Bool
  ||| Renaming rules for arguments where the name of the argument does not
  ||| match the correspondent key in the translated JSON object.
  renames : List (String, String)
  ||| Fields that must be present in the JSON translation but have static
  ||| values.
  staticFields : List (String, JSON)

public export
defaultOpts : JSONDeriveOpts
defaultOpts = MkOpts False [] []

stripNs : Name -> Name
stripNs (NS _ x) = x
stripNs x = x

covering
genReadableSym : String -> Elab Name
genReadableSym hint = do
  MN v i <- genSym hint
    | _ => fail "cannot generate readable argument name"
  pure $ UN (v ++ show i)

var : Name -> TTImp
var = IVar EmptyFC

bindvar : String -> TTImp
bindvar = IBindVar EmptyFC

primStr : String -> TTImp
primStr = IPrimVal EmptyFC . Str

patClause : TTImp -> TTImp -> Clause
patClause = PatClause EmptyFC

implicit' : TTImp
implicit' = Implicit EmptyFC True

-- TODO: add support for polymorphic types and maybe use another type for
-- optional fields in place of Maybe.
||| Automatic derivation of `ToJSON` instances.
||| NOTE: all the fields in each constructor MUST be named, record already
||| comply but types declared with data must have constructors declared like
||| this:
||| ```idris example
||| data Position : Type where
|||   MkPosition : (x : Integer) -> (y : Integer) -> Position
||| ```
||| If the tagging option is enabled, types with multiple constructors are
||| translated to a JSON object with a single key-value pair where the key is
||| constructor name (without the namespace) and the value is the JSON object
||| translated as if untagged.
||| Constructor arguments that are `Maybe` instances are omitted if `Nothing`
||| and converted without the constructor if `Just`. If you need to translate a
||| mandatory field that can be nullable use the `Null` type.
|||
||| @ opts The automatic derivation options.
||| @ name The name of the type to derive for. Can be without namespace if unambigous.
public export covering
deriveToJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab ()
deriveToJSON opts n = do
    [(name, imp)] <- getType n
      | xs => fail $ show n ++ " must be in scope and unique. Possible referred types are: " ++ show (fst <$> xs)
    -- FIXME: temporary name for debugging, should be converted to a name impossible to define from users
    -- and should not be exported, unless a specific option is enabled.
    let funName = UN ("toJSON" ++ show (stripNs n))
    let objName = UN ("__impl_toJSON" ++ show (stripNs n))
    conNames <- getCons name
    cons <- for conNames $ \n => do
      [(conName, conImpl)] <- getType n
        | _ => fail $ show n ++ " constructor must be in scope and unique"
      (bindNames, rhs) <- genRHS conImpl
      let rhs = if opts.tagged
                   then `(JObject $ [MkPair ~(primStr $ show $ stripNs n) (JObject $ catMaybes ~rhs)])
                   else `(JObject $ catMaybes ~rhs)
      let lhs = `(~(var funName) ~(applyBinds (var conName) (reverse bindNames)))
      pure $ patClause lhs rhs
    let funclaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(~(var name) -> JSON))
    let fundecl = IDef EmptyFC funName cons
    declare [funclaim, fundecl]
    [(ifName, _)] <- getType `{ToJSON}
      | _ => fail "ToJSON interface must be in scope and unique"
    [NS _ (DN _ ifCon)] <- getCons ifName
      | _ => fail "Interface constructor error"
    let retty = `(ToJSON ~(var name))
    let objclaim = IClaim EmptyFC MW Export [Hint True, Inline] (MkTy EmptyFC EmptyFC objName retty)
    let objrhs = `(~(var ifCon) ~(var funName))
    let objdecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)]
    declare [objclaim, objdecl]
  where
    genRHS : TTImp -> Elab (List Name, TTImp)
    genRHS (IPi _ _ _ (Just n) `(Prelude.Types.Maybe ~argTy) retTy) = do
      (ns, rest) <- genRHS retTy
      let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames
      pure (n :: ns, `(((MkPair ~name . toJSON) <$> ~(var n)) :: ~rest))
    genRHS (IPi _ _ _ (Just n) argTy retTy) = do
      (ns, rest) <- genRHS retTy
      let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames
      pure (n :: ns, `(Just (MkPair ~name (toJSON ~(var n))) :: ~rest))
    genRHS (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named"
    genRHS _ = do
      -- Hack required, because if you quote directly opts.staticFields the elaborator introduces unsolved holes
      r <- traverse (\(k, v) => (k,) <$> quote v) opts.staticFields
      pure ([], foldr (\(k, v), acc => `(Just (MkPair ~(primStr k) ~v) :: ~acc)) `([]) r)

    applyBinds : TTImp -> List Name -> TTImp
    applyBinds = foldr (\n, acc => `(~acc ~(bindvar $ show n)))

||| Automatic derivation of `FromJSON` instances.
||| NOTE: all the fields in each constructor MUST be named, record already
||| comply but types declared with data must have constructors declared like
||| this:
||| ```idris example
||| data Position : Type where
|||   MkPosition : (x : Integer) -> (y : Integer) -> Position
||| ```
||| If the tagging option is enabled, types with multiple constructors are
||| translated to a JSON object with a single key-value pair where the key is
||| constructor name (without the namespace) and the value is the JSON object
||| translated as if untagged.
||| Constructor arguments that are `Maybe` instances are omitted if `Nothing`
||| and converted without the constructor if `Just`. If you need to translate a
||| mandatory field that can be nullable use the `Null` type.
|||
||| @ opts The automatic derivation options.
||| @ name The name of the type to derive for. Can be without namespace if unambigous.
public export covering
deriveFromJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab ()
deriveFromJSON opts n = do
    [(name, imp)] <- getType n
      | xs => fail $ show n ++ " must be in scope and unique. Possible referred types are: " ++ show (fst <$> xs)
    -- FIXME: temporary name for debugging, should be converted to a name impossible to define from users
    -- and should not be exported, unless a specific option is enabled.
    let funName = UN ("fromJSON" ++ show (stripNs n))
    let objName = UN ("__impl_fromJSON" ++ show (stripNs n))
    conNames <- getCons name
    argName <- genReadableSym "arg"
    cons <- for conNames $ \n => do
      [(conName, conImpl)] <- getType n
        | _ => fail $ show n ++ "constructor must be in scope and unique"
      args <- getArgs conImpl
      pure (conName, args)
    clauses <- traverse (\(cn, as) => genClause funName cn argName (reverse as)) cons
    let clauses = if opts.tagged
                     then (uncurry patClause <$> clauses)
                     else [patClause `(~(var funName) (JObject ~(bindvar $ show argName)))
                                     (foldl (\acc, x => `(~x <|> ~acc)) `(Nothing) (snd <$> clauses))]
    let funClaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(JSON -> Maybe ~(var name)))
    let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~implicit') `(Nothing)])
    declare [funClaim, funDecl]
    [(ifName, _)] <- getType `{FromJSON}
      | _ => fail "FromJSON interface must be in scope and unique"
    [NS _ (DN _ ifCon)] <- getCons ifName
      | _ => fail "Interface constructor error"
    let retty = `(FromJSON ~(var name))
    let objClaim = IClaim EmptyFC MW Export [Hint True, Inline] (MkTy EmptyFC EmptyFC objName retty)
    let objrhs = `(~(var ifCon) ~(var funName))
    let objDecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)]
    declare [objClaim, objDecl]
  where
    getArgs : TTImp -> Elab (List (Name, TTImp))
    getArgs (IPi _ _ _ (Just n) argTy retTy) = ((n, argTy) ::) <$> getArgs retTy
    getArgs (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named"
    getArgs _ = pure []

    genClause : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp, TTImp)
    genClause funName t m xs = do
      let lhs = `(~(var funName) (JObject [MkPair ~(primStr $ show $ stripNs t) (JObject ~(bindvar $ show m))]))
      let rhs = foldr (\(n, type), acc => let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames in
                                              case type of
                                                   `(Prelude.Types.Maybe _) => `(~acc <*> (pure $ lookup ~name ~(var m) >>= fromJSON))
                                                   _ => `(~acc <*> (lookup ~name ~(var m) >>= fromJSON)))
                      `(pure ~(var t)) xs
      r <- traverse (\(k, v) => (k,) <$> quote v) opts.staticFields
      let rhs = foldr (\(k, v), acc => `((lookup ~(primStr k) ~(var m) >>= (guard . (== ~v))) *> ~acc)) rhs r
      pure (lhs, rhs)

||| Automatic derivation of `ToJSON` and `FromJSON` instances.
||| See `deriveToJSON` and `deriveFromJSON`.
|||
||| @ opts The automatic derivation options.
||| @ name The name of the type to derive for. Can be without namespace if unambigous.
public export covering
deriveJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab ()
deriveJSON opts name = deriveToJSON opts name *> deriveFromJSON opts name


text:
module Data.List.Algebra

import Control.Algebra
import Data.List

%default total

public export
SemigroupV (List ty) where
  semigroupOpIsAssociative = appendAssociative

public export
MonoidV (List ty) where
  monoidNeutralIsNeutralL = appendNilRightNeutral
  monoidNeutralIsNeutralR _ = Refl


text:
module Logic.Classic

import Logic.Basic

%access public
%default total

to_dne : a -> Not (Not a)
to_dne x y = y x

elim_dne : Not (Not a) -> a -- ((a -> _|_) -> _|_) -> a
elim_dne = ?elim_dne_1

em : Not a \/ a
em = ?em_1

peirce : ((p -> q) -> p) -> p   -- C.P.S!C.P.S!
peirce f = believe_me (\k => k (f k))

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy