text:
module Idris.Codegen.ExtSTG.JSON -- where

import Data.Strings
import Idris.Codegen.ExtSTG.STG
import Language.JSON.Data

{-
TODO: This could be autogenerated?
-- In many cases yes using proofsearch %search
-}

export
interface ToJSON a where
  toJSON : a -> JSON

export
ToJSON a => ToJSON (List a) where
  toJSON as = JArray (map toJSON as)

export
(ToJSON a, ToJSON b) => ToJSON (a, b) where
  toJSON (a, b) = JArray [toJSON a, toJSON b]

export
-- This is a special case in the Haskell AEson library used by Ext-STG JSON.
ToJSON a => ToJSON (Maybe a) where
  toJSON Nothing = JNull
  toJSON (Just a) = toJSON a

export
ToJSON String where
  toJSON = JString

ToJSON Bool where
  toJSON = JBoolean

ToJSON Char where
  toJSON c = JString (singleton c)

ToJSON Double where
  toJSON = JNumber

ToJSON Nat where
  toJSON n = JNumber (cast n)

ToJSON Int where
  toJSON i = JNumber (cast i)

ToJSON Integer where
  toJSON i = JNumber (cast i)

ToJSON FilePath where
  toJSON = JString . getFilePath

ToJSON UnitId where
  toJSON u = JObject [ ("getUnitId", toJSON (GetUnitId u)) ]

ToJSON ModuleName where
  toJSON m = JObject [ ("getModuleName", toJSON (GetModuleName m)) ]

ToJSON ForeignStubs where
  toJSON NoStubs = JObject
    [ ("tag", toJSON "NoStubs") ]
  toJSON (MkForeignStubs h s) = JObject
    [ ("tag", toJSON "ForeignStubs")
    , ("fsCHeader", toJSON h)
    , ("fsCSource", toJSON s)
    ]

ToJSON BufSpan where
  toJSON b = JObject
    [ ("bufSpanStart", toJSON (BufSpanStart b))
    , ("bufSpanEnd", toJSON (BufSpanEnd b))
    ]

ToJSON RealSrcSpan where
  toJSON r = JObject
    [ ("srcSpanFile"  , toJSON (SpanFile  r))
    , ("srcSpanSLine" , toJSON (SpanSLine r))
    , ("srcSpanSCol"  , toJSON (SpanSCol  r))
    , ("srcSpanELine" , toJSON (SpanELine r))
    , ("srcSpanECol"  , toJSON (SpanECol  r))
    ]

-- Because of different names in STG rep in Ext-STG, we need different tags.
ToJSON SrcSpan where
  toJSON (SsRealSrcSpan r m) = JObject
    [ ("tag", JString "RealSrcSpan") -- TODO: Rename constructor
    , ("contents", JArray [toJSON r, toJSON m])
    ]
  toJSON (SsUnhelpfulSpan n) = JObject
    [ ("tag", JString "UnhelpfulSpan")
    , ("contents", toJSON n)
    ]

ToJSON Unique where
  toJSON (MkUnique c i) = JArray [toJSON c, toJSON i]

ToJSON (DataConId r) where
  toJSON (MkDataConId u) = toJSON u

ToJSON DataConIdSg where
  toJSON (r ** d) = toJSON d

ToJSON TyConId where
  toJSON (MkTyConId u) = toJSON u

ToJSON ForeignSrcLang where
  toJSON LangC      = JString "LangC"
  toJSON LangCxx    = JString "LangCxx"
  toJSON LangObjc   = JString "LangObjc"
  toJSON LangObjxcc = JString "LangObjxcc"
  toJSON LangAsm    = JString "LangAsm"
  toJSON RawObject  = JString "RawObject"

ToJSON IdDetails where
  toJSON (VanillaId)    = JObject [ ("tag", JString "VanillaId") ]
  toJSON (FExportedId)  = JObject [ ("tag", JString "FExportedId") ]
  toJSON (RecSelId)     = JObject [ ("tag", JString "RecSelId") ]
  toJSON (ClassOpId)    = JObject [ ("tag", JString "ClassOpId") ]
  toJSON (PrimOpId)     = JObject [ ("tag", JString "PrimOpId") ]
  toJSON (TickBoxOpId)  = JObject [ ("tag", JString "TickBoxOpId") ]
  toJSON (DFunId)       = JObject [ ("tag", JString "DFunId") ]
  toJSON (CoVarId)      = JObject [ ("tag", JString "CoVarId") ]
  toJSON (JoinId i) = JObject
    [ ("tag", JString "JoinId")
    , ("contents", toJSON i)
    ]
  toJSON (DataConWorkId d) = JObject
    [ ("tag", JString "DataConWorkId")
    , ("contents", toJSON d)
    ]
  toJSON (DataConWrapId d) = JObject
    [ ("tag", JString "DataConWrapId")
    , ("contents", toJSON d)
    ]

ToJSON Scope where
  toJSON LocalScope      = JString "LocalScope"
  toJSON GlobalScope     = JString "GlobalScope"
  toJSON HaskellExported = JString "HaskellExported"
  toJSON ForeignExported = JString "ForeignExported"

ToJSON UpdateFlag where
  toJSON ReEntrant    = JString "ReEntrant"
  toJSON Updatable    = JString "Updatable"
  toJSON SingleEntry  = JString "SingleEntry"

ToJSON PrimElemRep where
  toJSON Int8ElemRep    = JString "Int8ElemRep"
  toJSON Int16ElemRep   = JString "Int16ElemRep"
  toJSON Int32ElemRep   = JString "Int32ElemRep"
  toJSON Int64ElemRep   = JString "Int64ElemRep"
  toJSON Word8ElemRep   = JString "Word8ElemRep"
  toJSON Word16ElemRep  = JString "Word16ElemRep"
  toJSON Word32ElemRep  = JString "Word32ElemRep"
  toJSON Word64ElemRep  = JString "Word64ElemRep"
  toJSON FloatElemRep   = JString "FloatElemRep"
  toJSON DoubleElemRep  = JString "DoubleElemRep"

ToJSON PrimRep where
  toJSON VoidRep      = JObject [ ("tag", JString "VoidRep") ]
  toJSON LiftedRep    = JObject [ ("tag", JString "LiftedRep") ]
  toJSON UnliftedRep  = JObject [ ("tag", JString "UnliftedRep") ]
  toJSON Int8Rep      = JObject [ ("tag", JString "Int8Rep") ]
  toJSON Int16Rep     = JObject [ ("tag", JString "Int16Rep") ]
  toJSON Int32Rep     = JObject [ ("tag", JString "Int32Rep") ]
  toJSON Int64Rep     = JObject [ ("tag", JString "Int64Rep") ]
  toJSON IntRep       = JObject [ ("tag", JString "IntRep") ]
  toJSON Word8Rep     = JObject [ ("tag", JString "Word8Rep") ]
  toJSON Word16Rep    = JObject [ ("tag", JString "Word16Rep") ]
  toJSON Word32Rep    = JObject [ ("tag", JString "Word32Rep") ]
  toJSON Word64Rep    = JObject [ ("tag", JString "Word64Rep") ]
  toJSON WordRep      = JObject [ ("tag", JString "WordRep") ]
  toJSON AddrRep      = JObject [ ("tag", JString "AddrRep") ]
  toJSON FloatRep     = JObject [ ("tag", JString "FloatRep") ]
  toJSON DoubleRep    = JObject [ ("tag", JString "DoubleRep") ]
  toJSON (VecRep n p) = JObject
    [ ("tag", JString "VecRep")
    , ("contents", JArray [toJSON n, toJSON p])
    ]

ToJSON RepType where
  toJSON (SingleValue p) = JObject
    [ ("tag", JString "SingleValue")
    , ("contents", toJSON p)
    ]
  toJSON (UnboxedTuple ps) = JObject
    [ ("tag", JString "UnboxedTuple")
    , ("contents", toJSON ps)
    ]
  toJSON PolymorphicRep = JObject
    [ ("tag", JString "PolymorphicRep")
    ]

ToJSON (BinderId r) where
  toJSON (MkBinderId u) = toJSON u

ToJSON BinderIdSg where
  toJSON (r ** b) = toJSON b

ToJSON (SBinder r) where
  toJSON b = JObject
    [ ("sbinderName"    , toJSON (binderName b))
    , ("sbinderId"      , toJSON (binderId b))
    , ("sbinderType"    , toJSON (binderRep b))
    , ("sbinderTypeSig" , toJSON "") -- Information field in ExtSTG
    , ("sbinderScope"   , toJSON (binderScope b))
    , ("sbinderDetails" , toJSON (binderDetails b))
    , ("sbinderInfo"    , toJSON (binderInfo b))
    , ("sbinderDefLoc"  , toJSON (binderDefLoc b))
    ]

ToJSON SBinderSg where
  toJSON (_ ** b) = toJSON b

ToJSON DataConRep where
  toJSON (AlgDataCon p) = JObject
    [ ("tag", JString "AlgDataCon")
    , ("contents", toJSON p)
    ]
  toJSON (UnboxedTupleCon p) = JObject
    [ ("tag", JString "UnboxedTupleCon")
    , ("contents", toJSON p)
    ]

mutual
  ToJSON STyCon where
    toJSON s = JObject
      [ ("stcName"    , toJSON (Name s))
      , ("stcId"      , toJSON (Id s))
      , ("stcDataCons", toJSON (DataCons s))
      , ("stcDefLoc"  , toJSON (DefLoc s))
      ]

  ToJSON (SDataCon r) where
    toJSON s = JObject
      [ ("sdcName" , toJSON (name s))
      , ("sdcId" , toJSON (ident s))
      , ("sdcRep" , toJSON (rep s))
      , ("sdcWorker" , toJSON (worker s))
      , ("sdcDefLoc" , toJSON (defLoc s))
      ]

  ToJSON SDataConSg where
    toJSON (r ** d) = toJSON d

ToJSON LitNumType where
  toJSON LitNumInt    = JString "LitNumInt"
  toJSON LitNumInt64  = JString "LitNumInt64"
  toJSON LitNumWord   = JString "LitNumWord"
  toJSON LitNumWord64 = JString "LitNumWord64"

ToJSON LabelSpec where
  toJSON (FunctionLabel i) = JObject
    [ ("tag", JString "FunctionLabel")
    , ("contents", toJSON i)
    ]
  toJSON DataLabel = JObject
    [ ("tag", JString "DataLabel")
    ]

ToJSON Lit where
  toJSON (LitChar c) = JObject
    [ ("tag", JString "LitChar")
    , ("contents", toJSON c)
    ]
  toJSON (LitString s) = JObject
    [ ("tag", JString "LitString")
    , ("contents", toJSON s)
    ]
  toJSON LitNullAddr = JObject
    [ ("tag", JString "LitNullAddr")
    ]
  toJSON (LitFloat d) = JObject
    [ ("tag", JString "LitFloat")
    , ("contents", toJSON d)
    ]
  toJSON (LitDouble d) = JObject
    [ ("tag", JString "LitDouble")
    , ("contents", toJSON d)
    ]
  toJSON (LitLabel s l) = JObject
    [ ("tag", JString "LitLabel")
    , ("contents", JArray [toJSON s, toJSON l])
    ]
  toJSON (LitNumber l i) = JObject
    [ ("tag", JString "LitNumber")
    , ("contents", JArray [toJSON l, toJSON i])
    ]

ToJSON (Arg r) where
  toJSON (StgVarArg i) = JObject
    [ ("tag"     , JString "StgVarArg")
    , ("contents", toJSON i)
    ]
  toJSON (StgLitArg l) = JObject
    [ ("tag", JString "StgLitArg")
    , ("contents", toJSON l)
    ]
  toJSON StgVoid = JObject
    [ ("tag", JString "StgVoid")
    ]

ToJSON ArgSg where
  toJSON (r ** x) = toJSON x

ToJSON SourceText where
  toJSON (MkSourceText s) = JObject
    [ ("tag", JString "MkSourceText")
    , ("contents", toJSON s)
    ]
  toJSON (NoSourceText) = JObject
    [ ("tag", JString "NoSourceText")
    ]

ToJSON CCallTarget where
  toJSON (StaticTarget t s u b) = JObject
    [ ("tag", JString "StaticTarget")
    , ("contents", JArray [toJSON t, toJSON s, toJSON u, toJSON b])
    ]
  toJSON DynamicTarget = JObject
    [ ("tag", JString "DynamicTarget")
    ]

ToJSON CCallConv where
  toJSON MkCCallConv        = JString "MkCCallConv"
  toJSON CApiConv           = JString "CApiConv"
  toJSON StdCallConv        = JString "StdCallConv"
  toJSON PrimCallConv       = JString "PrimCallConv"
  toJSON JavaScriptCallConv = JString "JavaScriptCallConv"

ToJSON Safety where
  toJSON PlaySafe           = JString "PlaySafe"
  toJSON PlayInterruptible  = JString "PlayInterruptible"
  toJSON PlayRisky          = JString "PlayRisky"

ToJSON ForeignCall where
  toJSON f = JObject
    [ ("foreignCTarget", toJSON (CTarget f))
    , ("foreignCConv"  , toJSON (CConv f))
    , ("foreignCSafety", toJSON (CSafety f))
    ]

ToJSON PrimCall where
  toJSON (MkPrimCall s u) = JArray [toJSON s, toJSON u]

{n : String} -> ToJSON (PrimOp n args ret) where
  toJSON p = JObject
    [ ("tag", JString "StgPrimOp")
    , ("contents", toJSON $ PrimOp.name p)
    ]

ToJSON StgOp where
  toJSON (StgPrimOp p) = JObject
    [ ("tag", JString "StgPrimOp")
    , ("contents", toJSON p)
    ]
  toJSON (StgPrimCallOp p) = JObject
    [ ("tag", JString "StgPrimCallOp")
    , ("contents", toJSON p)
    ]
  toJSON (StgFCallOp p) = JObject
    [ ("tag", JString "StgFCallOp")
    , ("contents", toJSON p)
    ]

ToJSON AltType where
  toJSON (PolyAlt) = JObject
    [ ("tag", JString "PolyAlt")
    ]
  toJSON (MultiValAlt i) = JObject
    [ ("tag", JString "MultiValAlt")
    , ("contents", toJSON i)
    ]
  toJSON (PrimAlt p) = JObject
    [ ("tag", JString "PrimAlt")
    , ("contents", toJSON p)
    ]
  toJSON (AlgAlt t) = JObject
    [ ("tag", JString "AlgAlt")
    , ("contents", toJSON t)
    ]

ToJSON (AltCon r) where
  toJSON (AltDataCon d) = JObject
    [ ("tag", JString "AltDataCon")
    , ("contents", toJSON d)
    ]
  toJSON (AltLit l) = JObject
    [ ("tag", JString "AltLit")
    , ("contents", toJSON l)
    ]
  toJSON AltDefault = JObject
    [ ("tag", JString "AltDefault")
    ]

toBinderList : {ps : List PrimRep} -> BList ps -> List SBinderSg
toBinderList []        = []
toBinderList (x :: xs) = mkSBinderSg x :: toBinderList xs

toConArgList : {ps : List PrimRep} -> ArgList ps -> List ArgSg
toConArgList [] = []
toConArgList (x :: xs) = mkArgSg x :: toConArgList xs

mutual

  ToJSON (Expr r) where
    toJSON (StgApp f a r) = JObject
      [ ("tag", JString "StgApp")
      , ("contents", JArray [toJSON f, toJSON a, toJSON r, JArray [toJSON "",toJSON "",toJSON ""]])
        -- ^^ Haskell implementation of the ExtSTG constains an extra field
        -- of type (String, String, String) for debugging, we don't have it here
        -- but when we generate the JSON it is needed on the Haskell side.
      ]
    toJSON (StgLit l) = JObject
      [ ("tag", JString "StgLit")
      , ("contents", toJSON l)
      ]
    toJSON (StgConApp {r=AlgDataCon []} d s) = JObject
      [ ("tag", JString "StgConApp")
      , ("contents", JArray [toJSON d, JArray [], JArray []])
        -- No (List RepType) is given, as we don't support UnboxedTuples for now.
      ]
    toJSON (StgConApp {r=AlgDataCon [p]} d s) = JObject
      [ ("tag", JString "StgConApp")
      , ("contents", JArray [toJSON d, JArray [toJSON s], JArray []])
        -- No (List RepType) is given, as we don't support UnboxedTuples for now.
      ]
    toJSON (StgConApp {r=AlgDataCon (p0 :: p1 :: ps)} d s) = JObject
      [ ("tag", JString "StgConApp")
      , ("contents", JArray [toJSON d, toJSON (toConArgList s), JArray []])
        -- No (List RepType) is given, as we don't support UnboxedTuples for now.
      ]
    toJSON (StgConApp {r=UnboxedTupleCon n} d s) impossible
    toJSON (StgOpApp {args=[]} {ret} p s) = JObject
      [ ("tag", JString "StgOpApp")
      , ("contents", JArray
            [ toJSON p
            , JArray []
            , toJSON (SingleValue ret)
            , toJSON (the (Maybe TyConId) Nothing)
            ])
      ]
    toJSON (StgOpApp {args=[a1]} {ret} p s) = JObject
      [ ("tag", JString "StgOpApp")
      , ("contents", JArray
            [ toJSON p
            , JArray [toJSON s]
            , toJSON (SingleValue ret)
            , toJSON (the (Maybe TyConId) Nothing)
            ])
      ]
    toJSON (StgOpApp {args=(a1::a2::as)} {ret} p s) = JObject
      [ ("tag", JString "StgOpApp")
      , ("contents", JArray
            [ toJSON p
            , toJSON (toConArgList s)
            , toJSON (SingleValue ret)
            , toJSON (the (Maybe TyConId) Nothing)
            ])
      ]
    toJSON (StgCase d s i a) = JObject
      [ ("tag", JString "StgCase")
      , ("contents", JArray [toJSON s, toJSON i, toJSON d, toJSON a])
        -- The order of the contents is important for the ExtSTG compatibility
      ]
    toJSON (StgLet b e) = JObject
      [ ("tag", JString "StgLet")
      , ("contents", JArray [toJSON b, toJSON e])
      ]
    toJSON (StgLetNoEscape b e) = JObject
      [ ("tag", JString "StgLetNoEscape")
      , ("contents", JArray [toJSON b, toJSON e])
      ]

  ToJSON (Alt r q) where
    toJSON (MkAlt AltDefault () body) = JObject
      [ ("altCon"    , toJSON (the (AltCon r) AltDefault))
      , ("altBinders", JArray [])
      , ("altRHS"    , toJSON body)
      ]
    toJSON (MkAlt (AltLit l) () body) = JObject
      [ ("altCon"    , toJSON (AltLit l))
      , ("altBinders", JArray [])
      , ("altRHS"    , toJSON body)
      ]
    toJSON (MkAlt (AltDataCon ((UnboxedTupleCon _) ** _)) unboxed body) impossible
    toJSON (MkAlt alt@(AltDataCon ((AlgDataCon []) ** _)) binders body) = JObject
      [ ("altCon"    , toJSON alt)
      , ("altBinders", JArray [])
      , ("altRHS"    , toJSON body)
      ]
    toJSON (MkAlt alt@(AltDataCon ((AlgDataCon [p]) ** _)) binder body) = JObject
      [ ("altCon"    , toJSON alt)
      , ("altBinders", JArray [toJSON binder])
      , ("altRHS"    , toJSON body)
      ]
    toJSON (MkAlt alt@(AltDataCon ((AlgDataCon (p0 :: p1 :: ps)) ** dc)) binders body) = JObject
      [ ("altCon"    , toJSON alt)
      , ("altBinders", toJSON $ toBinderList binders)
      , ("altRHS"    , toJSON body)
      ]

  ToJSON Rhs where
    toJSON (StgRhsClosure u a b) = JObject
      [ ("tag", JString "StgRhsClosure")
      , ("contents", JArray [JArray [], toJSON u, toJSON a, toJSON b])
      ]
    toJSON (StgRhsCon d a) = JObject
      [ ("tag", JString "StgRhsCon")
      , ("contents", JArray [toJSON d, toJSON a])
      ]

  ToJSON Binding where
    toJSON (StgNonRec i r) = JObject
      [ ("tag", JString "StgNonRec")
      , ("contents", JArray [toJSON i, toJSON r])
      ]
    toJSON (StgRec bs) = JObject
      [ ("tag", JString "StgRec")
      , ("contents", toJSON bs)
      ]

  export
  ToJSON TopBinding where
    toJSON (StgTopLifted b) = JObject
      [ ("tag"     , JString "StgTopLifted")
      , ("contents", toJSON b)
      ]
    toJSON (StgTopStringLit i l) = JObject
      [ ("tag", JString "StgTopStringLit")
      , ("contents", JArray [toJSON i, toJSON l])
      ]

export
ToJSON Module where
  toJSON m = JObject
    [ ("modulePhase"               , toJSON (Phase m))
    , ("moduleUnitId"              , toJSON (ModuleUnitId m))
    , ("moduleName"                , toJSON (Name m))
    , ("moduleSourceFilePath"      , toJSON (SourceFilePath m))
    , ("moduleForeignStubs"        , toJSON (ForeignStubs m))
    , ("moduleHasForeignExported"  , toJSON (HasForeignExported m))
    , ("moduleDependency"          , toJSON (Dependency m))
    , ("moduleExternalTopIds"      , toJSON (ExternalTopIds m))
    , ("moduleTyCons"              , toJSON (TyCons m))
    , ("moduleTopBindings"         , toJSON (TopBindings m))
    , ("moduleForeignFiles"        , toJSON (ForeignFiles m))
    ]

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
data TakeN: List a -> Type where
     Fewer: TakeN xs
     Exact: (nXs: List a) -> TakeN (nXs ++ rest)

total takeN: (n: Nat) -> (xs: List a) -> TakeN xs
takeN Z xs = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) = case takeN k xs of
  Fewer     => Fewer
  Exact nXs => Exact (x :: nXs)

groupByN: (n: Nat) -> (xs: List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs            | Fewer     = [xs]
  groupByN n (nXs ++ rest) | Exact nXs = nXs :: groupByN n rest

halves: List a -> (List a, List a)
halves xs =
  let
    halfLen = div (length xs) 2
  in
    splitInHalf halfLen xs
  where
    splitInHalf: Nat -> List a -> (List a, List a)
    splitInHalf n xs with (takeN n xs)
      splitInHalf n xs            | Fewer     = ([], xs)
      splitInHalf n (nXs ++ rest) | Exact nXs = (nXs, rest)

example: List Int
example = [1,2,3,4,5,6,7,8,9]

emptyList: List Int
emptyList = []

ext: idr

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Day1a

import System.File
import Data.Strings
import Data.Either
import Data.List
import Data.List.Quantifiers
import Data.List.Elem
import Decidable.Equality
import Data.Void

-- Convert Either to have Strings for the error case
stringEither : Show a => Either a b -> Either String b
stringEither = bimap show id

-- Convert Dec into Either
decEither : Dec a -> Either String a
decEither (Yes a) = Right a
decEither (No b) = Left "No solution"

-- Print the value of an Either, or its error string
ePrint : Show a => Either String a -> IO ()
ePrint ma = case ma of
  Left e => putStrLn ("ERROR: " ++ e)
  Right x => putStrLn (show x)

-- Helper function to read a file into a bunch of integers
readInput : HasIO io => String -> io (Either String (List Int))
readInput filename = do
  mContents <- stringEither <$> readFile filename
  pure $ do
    lines <- lines <$> mContents
    traverse (\line => maybeToEither "Bad int" (parseInteger line)) lines

-- Helper to convert from List Any proofs to Elem**prop proofs
anyElem : {0 p : a -> Type} -> {l : List a} -> Any p l -> (x : a ** (Elem x l, p x))
anyElem {l = x :: xs} (Here pf) = MkDPair x (Here, pf)
anyElem {l = x :: xs} (There pf) with (anyElem pf)
  anyElem {l = x :: xs} (There pf) | (el ** (elin , elpf)) = (el ** (There elin , elpf))

elemAny : {0 p : a -> Type} -> {l : List a} -> {x : a} -> Elem x l -> p x -> Any p l
elemAny Here px = Here px
elemAny (There y) px = There (elemAny y px)

--What does a certificate of a solution look like?
--Given an input list of integers, it's a solution, with a pair of two integers,
--  proofs that they were both in the input, a proof that they
-- sum to 2020, and a proof that the solution is their product.
-- Everything is irrelevant at runtime except the actual number

record Soln (l : List Int) where
  constructor MkSoln
  {soln : Int}
  {0 entry1 : Int}
  {0 entry2 : Int}
  0 in1 : Elem entry1 l
  0 in2 : Elem entry2 l
  0 sum2020 : entry1 + entry2 = 2020
  0 solnProduct : entry1 * entry2 = soln

-- Given an integer and a list, decide whether any of the integers
-- in the list sum to 2020 with the given int
find2020Partner : (l : List Int) ->(i : Int)  -> Dec (Any (\i2 => i + i2 = 2020) l)
find2020Partner l i = any (\i2 => decEq (i + i2) 2020) l

--Given a list, decide whether any integer in the list has a partner
-- that will sum to 2020
find2020Pair : (l : List Int) -> Dec (Any (\i1 => Any (\i2 => i1 + i2 = 2020) l) l)
find2020Pair l = any (find2020Partner l) l

--Given a proof that there is a pair satisfying the property, make a proper
--solution record
makeSoln :
   (l : List Int)
   -> Any (\i1 => Any (\i2 => i1 + i2 = 2020) l) l
   -> Soln l
makeSoln l anyPf with (anyElem anyPf)
  makeSoln l anyPf  | (i1 ** (elem1 , anyPf2)) with (anyElem anyPf2)
    makeSoln l anyPf  | (i1 ** (elem1 , anyPf2)) | (i2 ** (elem2 , sumPr)) =
      MkSoln elem1 elem2 sumPr Refl

-- Given a list of integers, determine whether there is a solution
-- to the problem, given that list
find2020Soln : (l : List Int) -> Dec (Soln l)
find2020Soln inputs = case find2020Pair inputs of
  Yes pf => Yes (makeSoln inputs pf)
  No npf => No (\ (MkSoln in1 in2 eq _) => absurdity (npf $ elemAny in1 $ elemAny in2 eq))

-- Parse our input, find the solution, then print it
main : IO ()
main = do
  mInts <- readInput "Day1a.in"
  ePrint $ do
    ints <- mInts
    solnCert <- decEither $ find2020Soln ints
    pure (soln solnCert)


text:
module WithProof

%default total

filter : (p : a -> Bool) -> (xs : List a) -> List a
filter p [] = []
filter p (x :: xs) with (p x)
  filter p (x :: xs) | False = filter p xs
  filter p (x :: xs) | True = x :: filter p xs

filterSquared : (p : a -> Bool) -> (xs : List a) ->
                filter p (filter p xs) === filter p xs
filterSquared p [] = Refl
{-
filterSquared p (x :: xs) with (p x)
  filterSquared p (x :: xs) | False = filterSquared p xs -- easy
  filterSquared p (x :: xs) | True = ?a
     -- argh! stuck on another with-block casing on (p x)!
     -- we could check (p x) again but how do we prove it
     -- can only ever be `True`?!
-}
filterSquared p (x :: xs) with (p x) proof eq
  filterSquared p (x :: xs) | False = filterSquared p xs -- easy
  filterSquared p (x :: xs) | True
    = rewrite eq in cong (x ::) (filterSquared p xs)


text:
module Arduino.Raw

import public Arduino.Time
import Arduino.Util

import Control.Monad.Coop
import Control.Monad.Trans

%default total

-----------------
--- Interface ---
-----------------

public export
interface LowLevelArduino m where
  digitalWrite : Bits8 -> Bits8 -> m Unit
  pinMode      : Bits8 -> Bits8 -> m Unit

---------------------------------------
--- Real (hardware) implementations ---
---------------------------------------

%foreign "C:digitalWrite,libarduino"
prim_digitalWrite : Bits8 -> Bits8 -> PrimIO Unit

%foreign "C:pinMode,libarduino"
prim_pinMode : Bits8 -> Bits8 -> PrimIO Unit

export
LowLevelArduino IO where
  digitalWrite = primIO ... prim_digitalWrite
  pinMode      = primIO ... prim_pinMode

%foreign "C:delay,libarduino"
prim_delay : Bits32 -> PrimIO Unit

export
DelayableFor IO where
  sleepFor = primIO . prim_delay . toMilliseconds

%foreign "C:millis,libarduino"
prim_millis : PrimIO Bits32

export
Timed IO where
  currentTime = fromMilliseconds <$> primIO prim_millis

-------------------------------
--- Lifting implementations ---
-------------------------------

export
(LowLevelArduino m, Monad m) => LowLevelArduino (Coop m) where
  digitalWrite = lift ... digitalWrite
  pinMode      = lift ... pinMode

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
word_lengths : List String -> List Nat
word_lengths [] = []
word_lengths (word :: words) = length word :: word_lengths words

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
||| Primitive monadic (non-transformer) parser
module Util.MiniParser
import Data.Vect

%default total
%access public export

data Parser a = P (String -> Either String (a, String))

parse :  Parser a -> String -> Either String (a, String)
parse (P f) str = f str

parseAll : Parser a -> String -> Either String a
parseAll p str = do
          (xa, rst) <- parse p str
          if rst == ""
          then Right xa
          else Left ("did not parse " ++ rst)

onechar : Parser Char
onechar = P (\inp => case strM inp of
                    StrNil => Left "Error! Parsing empty list."
                    StrCons x xs => Right (x, xs))

interface Parsable a where
  item : Parser a

Parsable Char where
   item = onechar

interface Parsable a => Composite b a where
   compose : List a -> b

Composite String Char where
   compose = pack

Functor Parser where
  map f p = P (\inp => case parse p inp of
                          Left err        => Left err
                          Right (v, rest) => Right ((f v), rest))

Applicative Parser where
  pure v  = P (\inp => Right (v, inp))
  a <*> b = P (\inp => do (f, rest ) <- parse a inp
                          (x, rest') <- parse b rest
                          pure ((f x), rest'))

Monad Parser where
  p >>= f = P (\inp => case parse p inp of
                         Left err       => Left err
                         Right (v,rest) => parse (f v) rest)

||| choice of parsers
Alternative Parser where
  empty   = P (const (Left "empty"))
  p <|> q = P (\inp => case parse p inp of
                         Left msg      => parse q inp
                         Right (v,out) => Right (v,out))

fail : String -> Parser a
fail msg = P (\_ => Left msg)

infix 0 <?>
||| similar to parsec allows to specify failure message
(<?>) : Parser a -> String -> Parser a
(<?>) p s = p <|> fail s

-- basic char parsers

accept : Parsable a => (a -> Bool) -> Parser a
accept f = do
         x <- item
         if (f x)
         then pure x
         else empty

digit : Parser Char
digit = accept isDigit

lower : Parser Char
lower = accept isLower

upper : Parser Char
upper = accept isUpper

letter : Parser Char
letter = accept isAlpha

char : Char -> Parser Char
char c = accept (c ==)

charIngoreCase : Char -> Parser Char
charIngoreCase c = accept ((toUpper c) ==) <|> accept ((toLower c) ==)

string : String -> Parser String
string s = map pack (traverse char (unpack s))

stringIngoreCase : String -> Parser String
stringIngoreCase s = map pack (traverse charIngoreCase (unpack s))

-- combinators

oneof : (Parsable a, Eq a) => List a -> Parser a
oneof xs = accept (\x => elem x xs)

optional : Parser a -> Parser (Maybe a)
optional p = map Just p <|> pure Nothing

notFollowedBy : Parser a -> Parser ()
notFollowedBy p = do
          a <- optional p
          case a of
            Nothing => pure ()
            Just x => fail "not empty"

eof : Parser ()
eof = notFollowedBy onechar

||| apply p only if q is not applicable
unless :  Parser a -> Parser a -> Parser a
unless q p = P (\inp => case parse q inp of
                        (Left _)  => parse p inp
                        (Right _) => Left "unless failed"
               )

exactly :  (n : Nat) -> Parser a  -> Parser (Vect n a)
exactly Z _      = pure Nil
exactly (S n) p = [| p :: exactly n p |]

covering
many : Parsable a => Parser a -> Parser (List a)
many p = do
  (Just i) <- optional p
    | Nothing => pure Nil
  [| pure i :: many p |]

covering
many1 : Parsable a => Parser a -> Parser (List a)
many1 p = do
    _ <- p
    many p

covering
spaces : Parser (List Char)
spaces = many1 (char ' ')

covering
until : Parser a -> Parser a -> Parser (List a)
until to p = map reverse (untilrec to p Nil)
   where
    partial
    untilrec : Parser a -> Parser a -> List a -> Parser (List a)
    untilrec to p xa = do
               i <- optional to
               case i of
                 Just _ => pure xa
                 Nothing => do
                   a <- p
                   untilrec to p (a :: xa)

covering
between : (Parsable a, Composite b a) => Parser a -> Parser a -> Parser b
between from to = do
        fx <- from
        as <- until to item
        pure (compose as)

covering
stringbetween : Parser Char -> Parser Char -> Parser String
stringbetween = between

-- primitive parsers

covering
decimalInt : Parser Int
decimalInt = many digit >>= pure . cast . pack

covering
decimalInteger : Parser Integer
decimalInteger = many digit >>= pure . cast . pack

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Marginalization

import Semiring
import HetVect
import Data.Morphisms

%default total
%access public export

prodFuncsV
  : Semiring n
  => {xs, ys: List Type}
  -> (Vect xs -> n)
  -> (Vect ys -> n)
  -> Vect (xs++ys)
  -> n
prodFuncsV {xs=[]} f g vs = f Nil * g vs
prodFuncsV {xs=x::xs} f g (y :: z) = prodFuncsV (f . (y::)) g z

||| A proof that every type in a given list belongs to a finite, bounded,
||| enumerable domain. Possibly better modelled in a more generic way (ie for
||| arbitrary constraints).
data AllFinite : List Type -> Type where
  Empty : AllFinite []
  Extra
    :  (rest : AllFinite xs)
    -> (MinBound x, MaxBound x, Enum x)
    => AllFinite (x::xs)

||| Maybe reformulate this in a tail-recursive way.
marg : (Semiring n, MinBound a, MaxBound a, Enum a) => (a -> n) -> n
marg f = sum (map f [minBound .. maxBound])

margOnce
  : (Semiring n, MinBound t, MaxBound t, Enum t)
  => (Vect (t::ts) -> n) -> (Vect ts -> n)
margOnce f = (applyMor . marg) (\x => Mor (f . (x::)))

margVec
  : Semiring n
  => {xs : List Type}
  -> {auto prf : AllFinite xs}
  -> (Vect xs -> n) -> n
margVec {xs=[]} f = f []
margVec {xs=x::xs} {prf=Extra rest} f = margVec (margOnce f)

margVecL
  : Semiring n
  => {xs, ys: List Type}
  -> {auto prf : AllFinite ys}
  -> (Vect (xs++ys) -> n)
  -> Vect xs -> n
margVecL f [] =  margVec f
margVecL f (x :: xs) = margVecL (\ys => f (x::ys)) xs

margVecR
  : Semiring n
  => {xs, ys: List Type}
  -> (Vect (xs++ys) -> n)
  -> {auto prf : AllFinite xs}
  -> Vect ys
  -> n
margVecR f = applyMor (margVec (\xs => Mor (\ys => f (xs++ys))))

finiteDistL
  : {xs, ys : List Type}
  -> (prf : AllFinite (xs++ys))
  -> AllFinite xs
finiteDistL {xs=[]} prf = Empty
finiteDistL {xs=x::xs} (Extra rest) = Extra (finiteDistL rest)

finiteDistR
  : {xs,ys : List Type}
  -> (prf : AllFinite (xs++ys))
  -> AllFinite ys
finiteDistR {xs=[]} prf = prf
finiteDistR {xs=x::xs} (Extra rest) = finiteDistR {xs} rest

-- elemConforms : {x : Type} -> {xs : List Type} -> (conform : AllFinite xs) -> (el : Elem x xs) -> Enum x
-- elemConforms (Extra rest) Here = Enum x
-- elemConforms conform (There x) = ?elemConforms_rhs_2

margVecAny
  :  Semiring n
  => {x : Type}
  -> {xs : List Type}
  -> (fin : AllFinite xs)
  -> (elem : Elem x xs)
  -> (Vect xs -> n)
  -> x -> n
margVecAny (Extra rest) Here f x = margVec {prf = rest} (f . (x::))
margVecAny (Extra rest) (There z) f x = margVecAny rest z (margOnce f) x

-- Can almost certainly be written quicker.
margAll
  :  Semiring s
  => {xs : List Type}
  -> {auto finite : AllFinite xs}
  -> curried xs s
  -> s
margAll = go where
  go
    :  Semiring s
    => {xs : List Type}
    -> {auto finite : AllFinite xs}
    -> curried xs s
    -> s
  go {finite = Empty} m = m
  go {finite = (Extra rest)} m =
    sum (map (go . m) [minBound .. maxBound])

prodFuncs
  : Semiring n
  => {xs: List Type}
  -> curried xs n
  -> curried xs n
  -> curried xs n
prodFuncs {xs=[]} x y = x * y
prodFuncs {n} {xs=x::xs} f g
  = \y => prodFuncs {n} {xs} (f y) (g y)

max_stars_repo_name: oisdk/belief-propagation-idris

max_issues_repo_name: oisdk/belief-propagation-idris

max_forks_repo_name: oisdk/belief-propagation-idris


text:
module Data.Fun.Extra

import Data.Fun
import Data.Rel
import Data.HVect

%default total

||| Apply an n-ary function to an n-ary tuple of inputs
public export
uncurry : {0 n : Nat} -> {0 ts : Vect n Type} -> Fun ts cod -> HVect ts -> cod
uncurry f [] = f
uncurry f (x::xs) = uncurry (f x) xs

||| Apply an n-ary function to an n-ary tuple of inputs
public export
curry : {n : Nat} -> {0 ts : Vect n Type} -> (HVect ts -> cod) -> Fun ts cod
curry {ts = []    } f = f []
curry {ts = _ :: _} f = \x => curry (\xs => f (x :: xs))

{-

The higher kind Type -> Type has a monoid structure given by
composition and the identity (Cayley). The type (n : Nat ** Vect n a)
has a monoid structure given by `(n, rs) * (m, ss) := (n + m, rs +
ss)` and `(0,[])`.

  `Fun' : (n : Nat ** Vect n Type) -> Type -> Type`

is then a monoid homomorphism between them. I guess this is some
instance of Cayley's theorem, but because of extensionality we can't
show we have an isomorphism.
-}
public export
homoFunNeut_ext : Fun [] cod -> id cod
homoFunNeut_ext x = x

public export
homoFunMult_ext : {n : Nat} -> {0 rs : Vect n Type} -> Fun (rs ++ ss) cod -> (Fun rs . Fun ss) cod
homoFunMult_ext {rs = []     }  gs = gs
homoFunMult_ext {rs = t :: ts} fgs = \x => homoFunMult_ext (fgs x)

public export
homoFunNeut_inv : id cod -> Fun [] cod
homoFunNeut_inv x = x

public export
homoFunMult_inv : {n : Nat} -> {0 rs : Vect n Type} -> (Fun rs . Fun ss) cod -> Fun (rs ++ ss) cod
homoFunMult_inv {rs = []     } gs = gs
homoFunMult_inv {rs = t :: ts} fgs = \x => homoFunMult_inv (fgs x)

||| Apply an n-ary function to an n-ary tuple of inputs
public export
applyPartially : {n : Nat} -> {0 ts : Vect n Type}
               -> Fun (ts ++ ss) cod -> (HVect ts -> Fun ss cod)
applyPartially fgs = uncurry {ts} {cod = Fun ss cod} (homoFunMult_ext {rs=ts} {ss} fgs)

{- -------- (slightly) dependent versions of the above ---------------
   As usual, type dependencies make everything complicated          -}

||| Apply an n-ary dependent function to its tuple of inputs (given by an HVect)
public export
uncurryAll : {0 n : Nat} -> {0 ts : Vect n Type} -> {0 cod : Fun ts Type}
        -> All ts cod -> (xs : HVect ts) -> uncurry cod xs
uncurryAll f [] = f
uncurryAll {ts = t :: ts} f (x :: xs) = uncurryAll {cod= cod x} (f x) xs

public export
curryAll : {n : Nat} -> {0 ts : Vect n Type} -> {0 cod : Fun ts Type}
        -> ((xs : HVect ts) -> uncurry cod xs)
        -> All ts cod
curryAll {ts = []     } f = f []
curryAll {ts = t :: ts} f = \x => curryAll (\ xs => f (x:: xs))

chainGenUncurried : {n : Nat} -> {0 ts : Vect n Type} -> {0 cod,cod' : Fun ts Type} ->
           ((xs : HVect ts) -> uncurry cod xs -> uncurry cod' xs) ->
           All ts cod -> All ts cod'
chainGenUncurried {ts = []} f gs = f [] gs
chainGenUncurried {ts = (t :: ts)} f gs = \x => chainGenUncurried (\u => f (x :: u)) (gs x)

public export
homoAllNeut_ext : Fun [] cod -> id cod
homoAllNeut_ext x = x

-- Not sure it's worth it getting the rest of Cayley's theorem to work

public export
extractWitness : {n : Nat} -> {0 ts : Vect n Type} -> {0 r : Rel ts} -> Ex ts r -> HVect ts
extractWitness {ts = []     }  _       = []
extractWitness {ts = t :: ts} (w ** f) = w :: extractWitness f

public export
extractWitnessCorrect : {n : Nat} -> {0 ts : Vect n Type} -> {0 r : Rel ts} -> (f : Ex ts r) ->
                        uncurry {ts} r (extractWitness {r} f)
extractWitnessCorrect {ts = []     } f = f
extractWitnessCorrect {ts = t :: ts} (w ** f) = extractWitnessCorrect f

public export
introduceWitness : {0 r : Rel ts} -> (witness : HVect ts) ->
                   uncurry {ts} r witness -> Ex ts r
introduceWitness []             f = f
introduceWitness (w :: witness) f = (w ** introduceWitness witness f)

----------------------------------------------------------------------
public export
data Pointwise : (r : a -> b -> Type) -> (ts : Vect n a) -> (ss : Vect n b) -> Type where
  Nil  : Pointwise r [] []
  (::) : {0 ss, ts : Vect n Type} ->
         (f : r t s) -> Pointwise r ts ss -> Pointwise r (t::ts) (s::ss)

public export
precompose : Pointwise (\a,b => a -> b) ts ss -> Fun ss cod -> Fun ts cod
precompose [] h = h
precompose (f :: fs) h = \x => precompose fs (h (f x))


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

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

module Interp

import Ast
import Data.List

%default partial

----------------------------------------------------------------------
-- Interpreter
----------------------------------------------------------------------

public export
Unifier : Type
Unifier = List (Variable, Term)

-- A non-lazy version of maybe
public export
maybe' : b -> (a -> b) -> Maybe a -> b
maybe' n j Nothing  = n
maybe' n j (Just x) = j x

public export
subs : Unifier -> Term -> Term
subs u (Var x)   = maybe' (Var x) id (lookup x u)
subs u (Comp n ts) = Comp n $ map (subs u) ts

public export
compose : Unifier -> Unifier -> Unifier
compose u1 u2 = (map (\(v, t) => (v, subs u2 t)) u1) ++ u2

public export
occursIn : Variable -> Term -> Bool
occursIn v (Var x)     = v == x
occursIn v (Comp _ ms) = any (occursIn v) ms

mutual
  public export
  covering
  unify : Term -> Term -> Maybe Unifier
  unify (Var "_") t                         = pure []
  unify t (Var "_")                         = pure []
  unify (Var x) (Var y) with (x == y)
     unify (Var x) (Var y) | True           = pure []
     _ | False = pure [(x, Var y)]
  unify (Var x) t with (not (x `occursIn` t))
      unify (Var x) t   | True              = pure [(x, t)]
      _ | False = Nothing
  unify t v@(Var _)                         = unify v t
  unify (Comp m ms) (Comp n ns) with (m == n)
     unify (Comp m ms) (Comp n ns) | True   = unifyList ms ns
     _ | False = Nothing
  unify _ _ = Nothing

  public export
  unifyList : Terms -> Terms -> Maybe Unifier
  unifyList (t :: ts) (r :: rs) =
      do u1 <- unify t r
         u2 <- unifyList (map (subs u1) ts) (map (subs u1) rs)
  -- Note: I'm not sure if Idris supports backtick notation for operators
         pure $ u1 `compose` u2
  unifyList [] [] = Just []
  unifyList _ _   = Nothing

mutual
  public export
  vars : Term -> List Variable
  vars (Var "_") = []
  vars (Var x) = [x]
  vars (Comp _ ts) = varsList ts

  public export
  varsList : Terms -> List Variable
  varsList ts = [ v | t <- ts, v <- vars t]

public export
variables : Terms -> List Variable
variables ts = nub $ varsList ts

public export
freshen : List Variable -> (Term, Terms) -> (Term, Terms)
freshen bound (tc, tb) = (subs sub tc, map (subs sub) tb)
  where
    vars : List Variable
    vars = variables (tc :: tb)
    nextVar : Int -> Variable -> Variable
    nextVar i v =
      let v' = "_" ++ show i ++ "_" ++ v in
        if v' `elem` bound
          then nextVar (i+1) v
          else v'
    sub : Unifier
    sub = [ (v, Var (nextVar 0 v)) | v <- vars, v `elem` bound]

public export
data Solution : Type where
    MkSolution : List (Variable, Term) -> Solution

public export
implementation Eq Solution where
    (MkSolution x) == (MkSolution y) = assert_total $ x == y

public export
Show Solution where
  show (MkSolution [])            = "True"
  show (MkSolution xs ) = (concat $ intersperse "\n" $ map renderBindings xs)
    where renderBindings : (Variable, Term) -> String
          renderBindings (v, t) = v ++ " = " ++ show t

public export
isPlain : List Char -> Bool
isPlain (c :: cs) = isLower c && all (\c => c == '_' || isAlphaNum c) cs
isPlain [] = False

public export
data SearchTree : Type where
  Sol : Solution -> SearchTree
  Node : Goal -> List SearchTree -> SearchTree

public export
Eq SearchTree where
  (Sol x) == (Sol y) = assert_total $ x == y
  (Node x y) == (Node x' y') = assert_total $ (x == x') && (y == y')
  x == y = False

public export
isReportGoal : Term -> Bool
isReportGoal (Comp "_report" _) = True
isReportGoal _                  = False

public export
getSolution : Term -> Solution
getSolution (Comp "_report" args) = MkSolution sol
    where nontriv : (String, Term) -> Bool
          nontriv (x, (Var y)) with (x == y)
            nontriv (x, (Var y)) | True = False
            nontriv (x, (Var y)) | _ = True
          nontriv _ = True
          sol : ?
          sol = filter nontriv $ map (\ (Comp "=" [Comp v [], t]) => (v, t)) args
getSolution _ = MkSolution [("ERROR", Var "_Error")]

-- Uses the List monad for backtracking
public export
solve : Program -> Goal -> List SearchTree
solve prog [r] with (isReportGoal r)
    solve prog [r] | True  =  pure $ Sol $ getSolution r
    solve prog [r] | False = []
solve prog g@(t1 :: ts) = pure $ Node g trees
    where
      trees : List SearchTree
      trees = do
        c <- prog
        let (tc, tsc) = freshen (variables g) c
        case unify tc t1 of
         Just u => do
           let g' = map (subs u) $ tsc ++ ts
           solve prog g'
         Nothing => []

public export
makeReportGoal : Terms -> List Term
makeReportGoal goal = [Comp "_report" reportVars]
    where vars : List Variable
          vars = variables goal
          reportVars : Terms
          reportVars = map (\ v => Comp "=" [Comp v [], Var v]) vars

-- Use the trick of inserting an extra reporting goal
public export
makeReportTree : Program -> Goal -> SearchTree
makeReportTree prog goal = Node goal $ solve prog (goal ++ makeReportGoal goal)

----------------------------------------------------------------------
-- Traveral of Search Trees
----------------------------------------------------------------------

-- Depth first
public export
dfs : SearchTree -> List Solution
dfs (Sol sols) = [sols]
dfs (Node _ st) = [ s | t <- st, s <- dfs t]

-- Breath first
public export
bfs : SearchTree -> List Solution
bfs t = trav [t]
    where trav : List SearchTree -> List Solution
          trav [] = []
          trav ((Sol x) :: q) = x :: trav q
          trav ((Node _ st)  :: q) = trav (q ++ st)

-- Limited depth first
public export
limitedDfs : Int -> SearchTree -> List Solution
limitedDfs _ (Sol sols)  = [sols]
limitedDfs 0 _           = []
limitedDfs n (Node _ st) = [ s | t <- st, s <- limitedDfs (n-1) t]

-----------------------------------------------------------------------
--- Syntax for the DSL ---
-----------------------------------------------------------------------

-- Note: I might actually want to do something here like apply some
-- function to "h" and "b" here in order to supply some more syntatic
-- sugar.

-- syntax [h] ":-" [b] = (h, b)
infix 10 :-
export
(:-) : Term -> Terms -> Clause
head :- body = (head, body)

public export
empty : List Term
empty = []

-- syntax [p] "." = (p, empty)
-- suffix 10 .

export
data ProgramElement = Term | Clause

export
interface InterpProgramElement type (0 p : ProgramElement) | type where
  toClause : type -> Clause

export
InterpProgramElement Term Term where
  toClause p = (p, empty)

export
InterpProgramElement Clause Clause where
  toClause = id

public export
data DSLProgram : Type where
  Nil : DSLProgram
  (::) : InterpProgramElement type p => type -> DSLProgram -> DSLProgram

export
unDSL : DSLProgram -> Program
unDSL [] = []
unDSL (element :: elements) = toClause element :: unDSL elements

-- syntax "?-" [q] = nub $ bfs $ makeReportTree program [q]

prefix 10 ?-
export
(?-) : {auto program : Program} -> Term -> List Solution
(?-) {program} q = nub $ bfs $ makeReportTree program [q]


text:
module Tr

import BoundAst
import Data.Fin
import Data.Vect
import Instances
import CodeGen

%default total

-- We do not have the ability to actually express type signatures like
--
--     (a -> b) -> f a -> f b
--
-- in F#. However, we can fake it out with these methods, which have no runtime
-- use; they are purely a typelevel hack to let us have a way to predicate
-- truths about a type via member constraints.
--
-- The `SameTypeCtr` set of functions allow us to define the idea that for some
-- `^a0` and `^b0`, that they are `f a` and `f b`, in the sense that the `f` is
-- in fact the same type constructor, regardless of the types it is
-- parameterized over.
--
-- The `IsParameterizedOver*` set of functions allow us to define the idea that
-- for some `^a0` and `^a`, they are in fact `f a` and `a` such that `a` is in
-- fact the same type in both cases.
--
-- Ultimately, both are just getting around the fact that you can't
-- "peek inside" a statically resolved type parameter in F#.

--data HKTPred
--  = SameTypeCtr
--  | IsParameterizedOver

-- If a method's type uses TypeAppl, it will need to make sure to include ^hkt
-- in the generated F# code, for injecting HKTPreds.
--
-- For every pair of distinct TypeAppl with the same type constructor, one
-- SameTypeCtr will need to be scheduled to be generated.
-- For every unique TypeAppl, one IsParameterizedOverA will need to be
-- scheduled to be generated.
--
-- The generated code will always need a ^tc argument for every time class involved.
-- The generated code will need a SRTP for every monotype and typeappl in the equation.

||| Monotype reworked to be based on n-arry (uncurried) type applications and
||| function types rather than curried
data Monotype'
  = Term' String
  | FuncType' Monotype' (Monotype', List Monotype')
  | NAryTypeAppl' (List Monotype')

cons : a -> (a, List a) -> (a, List a)
cons x (x', xs) = (x, x' :: xs)

mutual -- Total this way, fascinatingly enough
  unwindUnaryTypeOp : UnaryTypeOp -> List Monotype'
  unwindUnaryTypeOp TypeclassCtr = []
  unwindUnaryTypeOp (NAryTypeAppl uto mt) = breakIntoSubExprs mt :: unwindUnaryTypeOp uto

  clingShangHoong : Monotype -> (Monotype', List Monotype')
  clingShangHoong (Term x) = (Term' x, [])
  clingShangHoong (FuncType x y) = cons (breakIntoSubExprs x) (clingShangHoong y)
  clingShangHoong (TypeFullyApplied x y) = (breakIntoSubExprs $ TypeFullyApplied x y, [])

  breakIntoSubExprs : Monotype -> Monotype'
  breakIntoSubExprs (Term x) = Term' x
  breakIntoSubExprs (FuncType x y) = FuncType' (breakIntoSubExprs x) $ clingShangHoong y
  breakIntoSubExprs (TypeFullyApplied uto mt) =
    NAryTypeAppl' $ reverse $ breakIntoSubExprs mt :: unwindUnaryTypeOp uto

genVar : Nat -> String
genVar k =
  pack $ Stream.take (divNatNZ k 26 SIsNotZ + 1) $ repeat $ chr $ cast $ modNatNZ k 26 SIsNotZ + 97

genSRTPVar : Nat -> String
genSRTPVar k = "^" ++ genVar k

data LBranch = LeftBranch

parenthesize : String -> String
parenthesize s = "(" ++ s ++ ")"

maybeParenthesize : Maybe LBranch -> String -> String
maybeParenthesize = flip $ foldl $ flip $ \_ => parenthesize

parenthesizeVar : Nat -> String -> (Nat, String)
parenthesizeVar k s =
  (S k, parenthesize $ genVar k ++ " : " ++ s)

iAmIgnorant : Nat -> Maybe LBranch -> Monotype -> (Nat, String)
iAmIgnorant k _ (Term _) = (S k, genSRTPVar k)
iAmIgnorant k branch (FuncType x y) =
  let (k0, s0) = iAmIgnorant k (Just LeftBranch) x
      (k1, s1) = iAmIgnorant k0 Nothing y
  in (k1, maybeParenthesize branch $ s0 ++ " -> " ++ s1)
iAmIgnorant k _ (TypeFullyApplied x y) = (S k, genSRTPVar k)

halp : Nat -> Nat -> Maybe LBranch -> Monotype -> String
halp k v _ (FuncType x y) =
  let (k0, s0) = iAmIgnorant k Nothing x
      (v0, s1) = parenthesizeVar v s0
  in s1 ++ " " ++ halp k0 v0 Nothing y
halp k v Nothing m = ": " ++ (snd $ iAmIgnorant k Nothing m)
halp k v (Just x) m = snd $ parenthesizeVar v $ snd $ iAmIgnorant k Nothing m

test : String
test = halp Z Z Nothing $ uncurry FuncType TrimapType

data Sep = Comma | Star

record FSGenericType where
  constructor FSGenType
  pre : String
  sep : Sep
  targs : List String
  post : String

consTArg : String -> FSGenericType -> FSGenericType
consTArg targ (FSGenType pre sep targs post) = (FSGenType pre sep (targ :: targs) post)

data SameTypeCtr
  = SameTypeCtr' FSGenericType FSGenericType

doubleConsTArg : String -> SameTypeCtr -> SameTypeCtr
doubleConsTArg targ (SameTypeCtr' x y) = (SameTypeCtr' (consTArg targ x) (consTArg targ y))

genNSRTPVarsFrom : Nat -> Nat -> List String
genNSRTPVarsFrom n k = toList $ take n $ map genSRTPVar $ iterate S k

FSTupleType : List String -> FSGenericType
FSTupleType targs = FSGenType "( " Star targs ")"

FSRegularType : String -> List String -> FSGenericType
FSRegularType name targs = FSGenType (name ++ "< ") Comma targs ">"

FSArrayType : String -> FSGenericType
FSArrayType x = FSGenType "" Comma [x] "[]"

pairedGenericTArgs : Nat -> Nat -> (List String, List String)
pairedGenericTArgs n k =
  (genNSRTPVarsFrom (minus n k) k, genNSRTPVarsFrom (minus n k) (k + n))

sameTypeCtr_ : Nat -> MMTypeCtr n -> SameTypeCtr
sameTypeCtr_ k (Regular n x) =
  let (targs0, targs1) = pairedGenericTArgs (n + 1) k
  in SameTypeCtr' (FSRegularType x targs0) (FSRegularType x targs1)
sameTypeCtr_ k (Tuple n) =
  let (targs0, targs1) = pairedGenericTArgs (n + 2) k
  in SameTypeCtr' (FSTupleType targs0) (FSTupleType targs1)
sameTypeCtr_ _ Array = SameTypeCtr' (FSArrayType "^a") (FSArrayType "^b")
sameTypeCtr_ k (Appl1 x) = doubleConsTArg (genSRTPVar k) $ sameTypeCtr_ (S k) x

TODO : String
TODO = genSMI $ sameTypeCtrToSMI $ sameTypeCtr $ Appl1 $ Appl1 $ Tuple 2
-- BAD result:
--  "  static member inline SameTypeCtr (_ : ( ^a * ^b * ^c * ^d), _ : ( ^a * ^b * ^g * ^h)) : unit = ()" : String
-- Without breaking
-- genSMI $ sameTypeCtrToSMI $ sameTypeCtr $ Tuple Z
-- Which gives the good result
--  "  static member inline SameTypeCtr (_ : ( ^a * ^b), _ : ( ^c * ^d)) : unit = ()" : String
-- Also need to start thinking about: A, B, etc...

sameTypeCtr : MMTypeCtr n -> SameTypeCtr
sameTypeCtr = sameTypeCtr_ Z

genSep : Sep -> String
genSep Comma = ", "
genSep Star = " * "

concatWith : Sep -> List String -> String
concatWith sep = concat . intersperse (genSep sep)

genFsGenType : FSGenericType -> String
genFsGenType (FSGenType pre sep targs post) =
  pre ++ concatWith sep targs ++ post

sameTypeCtrToSMI : SameTypeCtr -> SMI
sameTypeCtrToSMI (SameTypeCtr' x y) =
  StatMethInli "SameTypeCtr" ["_ : " ++ genFsGenType x, "_ : " ++ genFsGenType y] "unit" "()"

max_stars_repo_name: Kazark/tyclgen

max_issues_repo_name: Kazark/tyclgen

max_forks_repo_name: Kazark/tyclgen


text:
import Data.Vect

append_nil : Vect m elem -> Vect (plus m 0) elem
append_nil xs = rewrite plusZeroRightNeutral m in xs

append_xs : Vect (S (m + len)) elem -> Vect (m + (S len)) elem
append_xs xs = rewrite sym (plusSuccRightSucc m len) in xs

-- by "carelessly" changing `n + m` to `m + n` we need use a few rewrites
-- to prove to idris that the definition is valid
append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = append_nil ys
append (x :: xs) ys = append_xs (x :: append xs ys)


text:
module Main

import Data.Vect
import Data.Fin

import Lightyear
import Lightyear.Char
import Lightyear.Strings

test : Show a => Parser a -> String -> IO ()
test p input = case parse p input of
  Left  e => putStrLn e
  Right x => printLn x

listOf : Parser a -> Parser (List a)
listOf p = string "[" *!> (p `sepBy` string ",") <* string "]"

listOf' : Parser a -> Parser (List a)
listOf' p = brackets (commaSep p)

nat : Parser Nat
nat = integer

main : IO ()
main = do
  test nat "123"
  test (listOf nat) "[1,2,3,99]"
  test (listOf nat) "foo"
  test (listOf nat <|> (string "[foo" *> pure List.Nil)) "[foo"  -- should commit and fail
  test (listOf $ listOf nat) "[[1,2],[],[3,4,5]]"

  test (listOf' nat) "[1,2,3,99]"
  test (listOf' $ listOf' nat) "[[1,2],[],[3,4,5]]"
  test (listOf' nat <|> (string "[foo" *> pure List.Nil)) "[foo"  -- should commit and fail

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
module TTImp.Elab.Term

import Libraries.Data.UserNameMap

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Ambiguity
import TTImp.Elab.App
import TTImp.Elab.As
import TTImp.Elab.Binders
import TTImp.Elab.Case
import TTImp.Elab.Check
import TTImp.Elab.Dot
import TTImp.Elab.Hole
import TTImp.Elab.ImplicitBind
import TTImp.Elab.Lazy
import TTImp.Elab.Local
import TTImp.Elab.Prim
import TTImp.Elab.Quote
import TTImp.Elab.Record
import TTImp.Elab.Rewrite
import TTImp.Elab.RunElab
import TTImp.Reflect
import TTImp.TTImp

%default covering

-- If the expected type has an implicit pi, elaborate with leading
-- implicit lambdas if they aren't there already.
insertImpLam : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               Env Term vars ->
               (term : RawImp) -> (expected : Maybe (Glued vars)) ->
               Core RawImp
insertImpLam {vars} env tm (Just ty) = bindLam tm ty
  where
    -- If we can decide whether we need implicit lambdas without looking
    -- at the normal form, do so
    bindLamTm : RawImp -> Term vs -> Core (Maybe RawImp)
    bindLamTm tm@(ILam _ _ Implicit _ _ _) (Bind fc n (Pi _ _ Implicit _) sc)
        = pure (Just tm)
    bindLamTm tm@(ILam _ _ AutoImplicit _ _ _) (Bind fc n (Pi _ _ AutoImplicit _) sc)
        = pure (Just tm)
    bindLamTm tm@(ILam _ _ (DefImplicit _) _ _ _) (Bind fc n (Pi _ _ (DefImplicit _) _) sc)
        = pure (Just tm)
    bindLamTm tm (Bind fc n (Pi _ c Implicit ty) sc)
        = do n' <- genVarName (nameRoot n)
             Just sc' <- bindLamTm tm sc
                 | Nothing => pure Nothing
             pure $ Just (ILam fc c Implicit (Just n') (Implicit fc False) sc')
    bindLamTm tm (Bind fc n (Pi _ c AutoImplicit ty) sc)
        = do n' <- genVarName (nameRoot n)
             Just sc' <- bindLamTm tm sc
                 | Nothing => pure Nothing
             pure $ Just (ILam fc c AutoImplicit (Just n') (Implicit fc False) sc')
    bindLamTm tm (Bind fc n (Pi _ c (DefImplicit _) ty) sc)
        = do n' <- genVarName (nameRoot n)
             Just sc' <- bindLamTm tm sc
                 | Nothing => pure Nothing
             pure $ Just (ILam fc c (DefImplicit (Implicit fc False))
                                    (Just n') (Implicit fc False) sc')
    bindLamTm tm exp
        = case getFn exp of
               Ref _ Func _ => pure Nothing -- might still be implicit
               TForce _ _ _ => pure Nothing
               Bind _ _ (Lam _ _ _ _) _ => pure Nothing
               _ => pure $ Just tm

    bindLamNF : RawImp -> NF vars -> Core RawImp
    bindLamNF tm@(ILam _ _ Implicit _ _ _) (NBind fc n (Pi _ _ Implicit _) sc)
        = pure tm
    bindLamNF tm@(ILam _ _ AutoImplicit _ _ _) (NBind fc n (Pi _ _ AutoImplicit _) sc)
        = pure tm
    bindLamNF tm (NBind fc n (Pi fc' c Implicit ty) sc)
        = do defs <- get Ctxt
             n' <- genVarName (nameRoot n)
             sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
             sc' <- bindLamNF tm sctm
             pure $ ILam fc c Implicit (Just n') (Implicit fc False) sc'
    bindLamNF tm (NBind fc n (Pi fc' c AutoImplicit ty) sc)
        = do defs <- get Ctxt
             n' <- genVarName (nameRoot n)
             sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
             sc' <- bindLamNF tm sctm
             pure $ ILam fc c AutoImplicit (Just n') (Implicit fc False) sc'
    bindLamNF tm (NBind fc n (Pi _ c (DefImplicit _) ty) sc)
        = do defs <- get Ctxt
             n' <- genVarName (nameRoot n)
             sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
             sc' <- bindLamNF tm sctm
             pure $ ILam fc c (DefImplicit (Implicit fc False))
                              (Just n') (Implicit fc False) sc'
    bindLamNF tm sc = pure tm

    bindLam : RawImp -> Glued vars -> Core RawImp
    bindLam tm gty
        = do ty <- getTerm gty
             Just tm' <- bindLamTm tm ty
                | Nothing =>
                    do nf <- getNF gty
                       bindLamNF tm nf
             pure tm'
insertImpLam env tm _ = pure tm

-- Main driver for checking terms, after implicits have been added.
-- Implements 'checkImp' in TTImp.Elab.Check
checkTerm : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            RigCount -> ElabInfo ->
            NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) ->
            Core (Term vars, Glued vars)
checkTerm rig elabinfo nest env (IVar fc n) exp
    = -- It may actually turn out to be an application, if the expected
      -- type is expecting an implicit argument, so check it as an
      -- application with no arguments
      checkApp rig elabinfo nest env fc (IVar fc n) [] [] [] exp
checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
    = do n <- case p of
                   Explicit => genVarName "arg"
                   Implicit => genVarName "impArg"
                   AutoImplicit => genVarName "conArg"
                   (DefImplicit _) => genVarName "defArg"
         checkPi rig elabinfo nest env fc r p n argTy retTy exp
checkTerm rig elabinfo nest env (IPi fc r p (Just (UN Underscore)) argTy retTy) exp
    = checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
checkTerm rig elabinfo nest env (IPi fc r p (Just n) argTy retTy) exp
    = checkPi rig elabinfo nest env fc r p n argTy retTy exp
checkTerm rig elabinfo nest env (ILam fc r p (Just n) argTy scope) exp
    = checkLambda rig elabinfo nest env fc r p n argTy scope exp
checkTerm rig elabinfo nest env (ILam fc r p Nothing argTy scope) exp
    = do n <- genVarName "_"
         checkLambda rig elabinfo nest env fc r p n argTy scope exp
checkTerm rig elabinfo nest env (ILet fc lhsFC r n nTy nVal scope) exp
    = checkLet rig elabinfo nest env fc lhsFC r n nTy nVal scope exp
checkTerm rig elabinfo nest env (ICase fc scr scrty alts) exp
    = checkCase rig elabinfo nest env fc scr scrty alts exp
checkTerm rig elabinfo nest env (ILocal fc nested scope) exp
    = checkLocal rig elabinfo nest env fc nested scope exp
checkTerm rig elabinfo nest env (ICaseLocal fc uname iname args scope) exp
    = checkCaseLocal rig elabinfo nest env fc uname iname args scope exp
checkTerm rig elabinfo nest env (IUpdate fc upds rec) exp
    = checkUpdate rig elabinfo nest env fc upds rec exp
checkTerm rig elabinfo nest env (IApp fc fn arg) exp
    = checkApp rig elabinfo nest env fc fn [arg] [] []  exp
checkTerm rig elabinfo nest env (IAutoApp fc fn arg) exp
    = checkApp rig elabinfo nest env fc fn [] [arg] []  exp
checkTerm rig elabinfo nest env (IWithApp fc fn arg) exp
    = throw (GenericMsg fc "with application not implemented yet")
checkTerm rig elabinfo nest env (INamedApp fc fn nm arg) exp
    = checkApp rig elabinfo nest env fc fn [] [] [(nm, arg)] exp
checkTerm rig elabinfo nest env (ISearch fc depth) (Just gexpty)
    = do est <- get EST
         nm <- genName "search"
         expty <- getTerm gexpty
         sval <- searchVar fc rig depth (Resolved (defining est)) env nest nm expty
         pure (sval, gexpty)
checkTerm rig elabinfo nest env (ISearch fc depth) Nothing
    = do est <- get EST
         nmty <- genName "searchTy"
         ty <- metaVar fc erased env nmty (TType fc)
         nm <- genName "search"
         sval <- searchVar fc rig depth (Resolved (defining est)) env nest nm ty
         pure (sval, gnf env ty)
checkTerm rig elabinfo nest env (IAlternative fc uniq alts) exp
    = checkAlternative rig elabinfo nest env fc uniq alts exp
checkTerm rig elabinfo nest env (IRewrite fc rule tm) exp
    = checkRewrite rig elabinfo nest env fc rule tm exp
checkTerm rig elabinfo nest env (ICoerced fc tm) exp
    = checkTerm rig elabinfo nest env tm exp
checkTerm rig elabinfo nest env (IBindHere fc binder sc) exp
    = checkBindHere rig elabinfo nest env fc binder sc exp
checkTerm rig elabinfo nest env (IBindVar fc n) exp
    = checkBindVar rig elabinfo nest env fc (Basic n) exp
checkTerm rig elabinfo nest env (IAs fc nameFC side n_in tm) exp
    = checkAs rig elabinfo nest env fc nameFC side n_in tm exp
checkTerm rig elabinfo nest env (IMustUnify fc reason tm) exp
    = checkDot rig elabinfo nest env fc reason tm exp
checkTerm rig elabinfo nest env (IDelayed fc r tm) exp
    = checkDelayed rig elabinfo nest env fc r tm exp
checkTerm rig elabinfo nest env (IDelay fc tm) exp
    = checkDelay rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IForce fc tm) exp
    = checkForce rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuote fc tm) exp
    = checkQuote rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuoteName fc n) exp
    = checkQuoteName rig elabinfo nest env fc n exp
checkTerm rig elabinfo nest env (IQuoteDecl fc ds) exp
    = checkQuoteDecl rig elabinfo nest env fc ds exp
checkTerm rig elabinfo nest env (IUnquote fc tm) exp
    = throw (GenericMsg fc "Can't escape outside a quoted term")
checkTerm rig elabinfo nest env (IRunElab fc tm) exp
    = checkRunElab rig elabinfo nest env fc tm exp
checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp
    = do let (cval, cty) = checkPrim {vars} fc c
         checkExp rig elabinfo env fc cval (gnf env cty) exp
checkTerm rig elabinfo nest env (IType fc) exp
    = checkExp rig elabinfo env fc (TType fc) (gType fc) exp

checkTerm rig elabinfo nest env (IHole fc str) exp
    = checkHole rig elabinfo nest env fc (Basic str) exp
checkTerm rig elabinfo nest env (IUnifyLog fc lvl tm) exp
    = withLogLevel lvl $ check rig elabinfo nest env tm exp
checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)
    = do nm <- genName "_"
         expty <- getTerm gexpty
         metaval <- metaVar fc rig env nm expty
         -- Add to 'bindIfUnsolved' if 'b' set
         when (b && bindingVars elabinfo) $
            do est <- get EST
               expty <- getTerm gexpty
               -- Explicit because it's an explicitly given thing!
               put EST (addBindIfUnsolved nm rig Explicit env metaval expty est)
         pure (metaval, gexpty)
checkTerm rig elabinfo nest env (Implicit fc b) Nothing
    = do nmty <- genName "implicit_type"
         ty <- metaVar fc erased env nmty (TType fc)
         nm <- genName "_"
         metaval <- metaVar fc rig env nm ty
         -- Add to 'bindIfUnsolved' if 'b' set
         when (b && bindingVars elabinfo) $
            do est <- get EST
               put EST (addBindIfUnsolved nm rig Explicit env metaval ty est)
         pure (metaval, gnf env ty)
checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
    = do -- enter the scope -> add unambiguous names
         est <- get EST
         rns <- resolveNames fc ns
         put EST $ record { unambiguousNames = mergeLeft rns (unambiguousNames est) } est

         -- inside the scope -> check the RHS
         result <- check rig elabinfo nest env rhs exp

         -- exit the scope -> restore unambiguous names
         newEST <- get EST
         put EST $ record { unambiguousNames = unambiguousNames est } newEST

         pure result
  where
    resolveNames : FC -> List Name -> Core (UserNameMap (Name, Int, GlobalDef))
    resolveNames fc [] = pure empty
    resolveNames fc (n :: ns) =
      case userNameRoot n of
        -- should never happen
        Nothing => throw $ InternalError $ "non-UN in \"with\" LHS: " ++ show n
        Just nRoot => do
          -- this will always be a global name
          -- so we lookup only among the globals
          ctxt <- get Ctxt
          rns <- lookupCtxtName n (gamma ctxt)
          case rns of
            []   => undefinedName fc n
            [rn] => insert nRoot rn <$> resolveNames fc ns
            _    => throw $ AmbiguousName fc (map fst rns)

-- Declared in TTImp.Elab.Check
-- check : {vars : _} ->
--         {auto c : Ref Ctxt Defs} ->
--         {auto m : Ref MD Metadata} ->
--         {auto u : Ref UST UState} ->
--         {auto e : Ref EST (EState vars)} ->
--         RigCount -> ElabInfo -> Env Term vars -> RawImp ->
--         Maybe (Glued vars) ->
--         Core (Term vars, Glued vars)
-- If we've just inserted an implicit coercion (in practice, that's either
-- a force or delay) then check the term with any further insertions
TTImp.Elab.Check.check rigc elabinfo nest env (ICoerced fc tm) exp
    = checkImp rigc elabinfo nest env tm exp
-- Don't add implicits/coercions on local blocks or record updates
TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILet _ _ _ _ _ _ _) exp
    = checkImp rigc elabinfo nest env tm exp
TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILocal _ _ _) exp
    = checkImp rigc elabinfo nest env tm exp
TTImp.Elab.Check.check rigc elabinfo nest env tm@(IUpdate _ _ _) exp
    = checkImp rigc elabinfo nest env tm exp
TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp
    = do defs <- get Ctxt
         est <- get EST
         tm <- expandAmbigName (elabMode elabinfo) nest env tm_in [] tm_in exp
         case elabMode elabinfo of
              InLHS _ => -- Don't expand implicit lambda on lhs
                 checkImp rigc elabinfo nest env tm exp
              _ => do tm' <- insertImpLam env tm exp
                      checkImp rigc elabinfo nest env tm' exp

onLHS : ElabMode -> Bool
onLHS (InLHS _) = True
onLHS _ = False

-- As above, but doesn't add any implicit lambdas, forces, delays, etc
-- checkImp : {vars : _} ->
--            {auto c : Ref Ctxt Defs} ->
--            {auto m : Ref MD Metadata} ->
--            {auto u : Ref UST UState} ->
--            {auto e : Ref EST (EState vars)} ->
--            RigCount -> ElabInfo -> Env Term vars -> RawImp -> Maybe (Glued vars) ->
--            Core (Term vars, Glued vars)
TTImp.Elab.Check.checkImp rigc elabinfo nest env tm exp
    = do res <- checkTerm rigc elabinfo nest env tm exp
         -- LHS arguments can't infer their own type - they need to be inferred
         -- from some other argument. This is to prevent arguments being not
         -- polymorphic enough. So, here, add the constraint to be checked later.
         when (onLHS (elabMode elabinfo) && not (topLevel elabinfo)) $
            do let (argv, argt) = res
               let Just expty = exp
                        | Nothing => pure ()
               addPolyConstraint (getFC tm) env argv !(getNF expty) !(getNF argt)
         pure res


text:
module Language.LSP.Message.Hover

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Markup
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
public export
record HoverClientCapabilities where
  constructor MkHoverClientCapabilities
  dynamicRegistration : Maybe Bool
  contentFormat : Maybe (List MarkupKind)
%runElab deriveJSON defaultOpts `{{HoverClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
public export
record HoverOptions where
  constructor MkHoverOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{HoverOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
public export
record HoverRegistrationOptions where
  constructor MkHoverRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{HoverRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
public export
record HoverParams where
  constructor MkHoverParams
  workDoneToken : Maybe ProgressToken
  textDocument : TextDocumentIdentifier
  position : Position
%runElab deriveJSON defaultOpts `{{HoverParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
public export
record Hover where
  constructor MkHover
  contents : OneOf [MarkedString, List MarkedString, MarkupContent]
  range : Maybe Range
%runElab deriveJSON defaultOpts `{{Hover}}


text:
||| GetLine
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module System.IO.Util.GetLine

import Data.Buffer

%default total

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

export mkGetLine' : HasIO io
                => (getc:io (Maybe Char))
                -> (buf:Buffer) -> (loc:Nat)
                -> io Nat
mkGetLine' getc buf loc = do
  bs <- rawSize buf
  if bs <= cast (natToInteger loc)
     then pure 0
     else go (fromInteger $ cast $ bs - cast loc) loc
  where
    go : Nat -> Nat -> io Nat
    go Z loc = pure loc
    go (S n) loc = do
      Just c <- getc
        | Nothing => pure loc
      if c == '\n'
         then pure loc
         else do
           setByte buf (cast loc) $ cast c
           go n (S loc)

export mkGetLine : HasIO io
               => (getc:io (Maybe Char))
               -> (maxlen:Nat)
               -> io (Maybe String)
mkGetLine getc maxlen = do
  Just b <- newBuffer (cast maxlen)
    | Nothing => pure Nothing
  newloc <- mkGetLine' getc b 0
  pure $ Just !(getString b 0 (cast newloc))

-- ---------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Control.App.Console

import public Control.App

public export
interface Console e where
  putStr : String -> App {l} e ()
  getStr : App {l} e String

export
PrimIO e => Console e where
  putStr str = primIO $ putStr str
  getStr = primIO $ getLine

export
putStrLn : Console e => String -> App {l} e ()
putStrLn str = putStr (str ++ "\n")


text:
module Data.List.Equalities

import Data.List

%default total

||| A list constructued using snoc cannot be empty.
export
snocNonEmpty : {x : a} -> {xs : List a} -> Not (xs ++ [x] = [])
snocNonEmpty {xs = []} prf = uninhabited prf
snocNonEmpty {xs = y :: ys} prf = uninhabited prf

||| Proof that snoc'ed list is not empty in terms of `NonEmpty`.
export %hint
SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (xs `snoc` x)
SnocNonEmpty []     _ = IsNonEmpty
SnocNonEmpty (_::_) _ = IsNonEmpty

||| Two lists are equal, if their heads are equal and their tails are equal.
export
consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
            x = y -> xs = ys -> x :: xs = y :: ys
consCong2 Refl Refl = Refl

||| Equal non-empty lists should result in equal components after destructuring 'snoc'.
export
snocInjective : {x : a} -> {xs : List a} -> {y : a} -> {ys : List a} ->
            (xs `snoc` x) = (ys `snoc` y) -> (xs = ys, x = y)
snocInjective {xs = []} {ys = []} Refl = (Refl, Refl)
snocInjective {xs = []} {ys = z :: zs} prf =
  let nilIsSnoc = snd $ consInjective {xs = []} {ys = zs ++ [y]} prf
   in void $ snocNonEmpty (sym nilIsSnoc)
snocInjective {xs = z :: xs} {ys = []} prf =
  let snocIsNil = snd $ consInjective {x = z} {xs = xs ++ [x]} {ys = []} prf
   in void $ snocNonEmpty snocIsNil
snocInjective {xs = w :: xs} {ys = z :: ys} prf =
  let (wEqualsZ, xsSnocXEqualsYsSnocY) = consInjective prf
      (xsEqualsYS, xEqualsY) = snocInjective xsSnocXEqualsYsSnocY
   in (consCong2 wEqualsZ xsEqualsYS, xEqualsY)

||| Appending pairwise equal lists gives equal lists
export
appendCong2 : {x1 : List a} -> {x2 : List a} ->
              {y1 : List b} -> {y2 : List b} ->
              x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2
appendCong2 {x1=[]} {y1=(_ :: _)} Refl _ impossible
appendCong2 {x1=(_ :: _)} {y1=[]} Refl _ impossible
appendCong2 {x1=[]} {y1=[]} _ eq2 = eq2
appendCong2 {x1=(_ :: _)} {y1=(_ :: _)} eq1 eq2 =
  let (hdEqual, tlEqual) = consInjective eq1
   in consCong2 hdEqual (appendCong2 tlEqual eq2)

||| List.map is distributive over appending.
export
mapDistributesOverAppend
  : (f : a -> b)
  -> (xs : List a)
  -> (ys : List a)
  -> map f (xs ++ ys) = map f xs ++ map f ys
mapDistributesOverAppend _ [] _ = Refl
mapDistributesOverAppend f (x :: xs) ys =
  cong (f x ::) $ mapDistributesOverAppend f xs ys

||| List.length is distributive over appending.
export
lengthDistributesOverAppend
  : (xs, ys : List a)
  -> length (xs ++ ys) = length xs + length ys
lengthDistributesOverAppend [] ys = Refl
lengthDistributesOverAppend (x :: xs) ys =
  cong S $ lengthDistributesOverAppend xs ys

||| Length of a snoc'd list is the same as Succ of length list.
export
lengthSnoc : (x : _) -> (xs : List a) -> length (snoc xs x) = S (length xs)
lengthSnoc x [] = Refl
lengthSnoc x (_ :: xs) = cong S (lengthSnoc x xs)

||| Appending the same list at left is injective.
export
appendSameLeftInjective : (xs, ys, zs : List a) -> zs ++ xs = zs ++ ys -> xs = ys
appendSameLeftInjective xs ys []      = id
appendSameLeftInjective xs ys (_::zs) = appendSameLeftInjective xs ys zs . snd . consInjective

||| Appending the same list at right is injective.
export
appendSameRightInjective : (xs, ys, zs : List a) -> xs ++ zs = ys ++ zs -> xs = ys
appendSameRightInjective xs ys [] = rewrite appendNilRightNeutral xs in
                                    rewrite appendNilRightNeutral ys in
                                    id
appendSameRightInjective xs ys (z::zs) = rewrite appendAssociative xs [z] zs in
                                         rewrite appendAssociative ys [z] zs in
                                         fst . snocInjective . appendSameRightInjective (xs ++ [z]) (ys ++ [z]) zs

||| List cannot be equal to itself prepended with some non-empty list.
export
appendNonEmptyLeftNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = xs ++ zs)
appendNonEmptyLeftNotEq []      (_::_)  Refl impossible
appendNonEmptyLeftNotEq (z::zs) (_::xs) prf
  = appendNonEmptyLeftNotEq zs (xs ++ [z]) @{SnocNonEmpty xs z}
  $ rewrite sym $ appendAssociative xs [z] zs in snd $ consInjective prf

||| List cannot be equal to itself appended with some non-empty list.
export
appendNonEmptyRightNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = zs ++ xs)
appendNonEmptyRightNotEq []      (_::_)  Refl impossible
appendNonEmptyRightNotEq (_::zs) (x::xs) prf = appendNonEmptyRightNotEq zs (x::xs) $ snd $ consInjective prf


text:
module Main

testlist : List (String, Int)
testlist = [("foo", 1), ("bar", 2)]

getVal : String -> a -> List (String, a) -> a
getVal x b xs = case lookup x xs of
                    Just v  => case lookup x xs of
                                    Just v' => v
                    Nothing => b

foo : (Int, String)
foo = (4, "foo")

ioVals : IO (String, String)
ioVals = do { pure ("First", "second") }

main : IO ()
main = do (a, b) <- ioVals
          putStr (a ++ " and " ++ b ++ "? ")
          let x = "bar"
          putStrLn (show (getVal x 7 testlist))
          let ((y, z) :: _) = testlist
          printLn z
          case lookup x testlist of
                 Just v => putStrLn (show v)
                 Nothing => putStrLn "Not there!"

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Minus

import Data.Nat

plus_mult : (n, m, k : Nat) -> {auto km : k `LTE` m} -> n + (m `minus` k) = (m + n) `minus` k
plus_mult n m Z = rewrite minusZeroRight m in
                  rewrite minusZeroRight $ m + n in
                  rewrite plusCommutative m n in
                  Refl
plus_mult n (S m) (S k) {km=LTESucc _} = plus_mult n m k

%hint
power2_ge_1 : (n : Nat) -> 1 `LTE` (2 `power` n)
power2_ge_1 Z     = LTESucc LTEZero
power2_ge_1 (S n) = lteTransitive (power2_ge_1 n) $ lteAddRight (2 `power` n)

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.Message.CallHierarchy

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.DocumentSymbols
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy
public export
record CallHierarchyClientCapabilities where
  constructor MkCallHierarchyClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{CallHierarchyClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy
public export
record CallHierarchyOptions where
  constructor MkCallHierarchyOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{CallHierarchyOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy
public export
record CallHierarchyRegistrationOptions where
  constructor MkCallHierarchyRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe String
%runElab deriveJSON defaultOpts `{CallHierarchyRegistrationOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy
public export
record CallHierarchyParams where
  constructor MkCallHierarchyParams
  workDoneToken : Maybe ProgressToken
  textDocument  : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{CallHierarchyParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy
public export
record CallHierarchyItem where
  constructor MkCallHierarchyItem
  name           : String
  kind           : SymbolKind
  tags           : Maybe (List SymbolTag)
  detail         : Maybe String
  uri            : DocumentURI
  range          : Range
  selectionRange : Range
  data_          : Maybe JSON
%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CallHierarchyItem}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_incomingCalls
public export
record CallHierarchyIncomingCallsParams where
  constructor MkCallHierarchyIncomingCallsParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  item               : CallHierarchyItem
%runElab deriveJSON defaultOpts `{CallHierarchyIncomingCallsParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_incomingCalls
public export
record CallHierarchyIncomingCall where
  constructor MkCallHierarchyIncomingCall
  from       : CallHierarchyItem
  fromRanges : List Range
%runElab deriveJSON defaultOpts `{CallHierarchyIncomingCall}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_outgoingCalls
public export
record CallHierarchyOutgoingCallsParams where
  constructor MkCallHierarchyOutgoingCallsParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  item               : CallHierarchyItem
%runElab deriveJSON defaultOpts `{CallHierarchyOutgoingCallsParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_outgoingCalls
public export
record CallHierarchyOutgoingCall where
  constructor MkCallHierarchyOutgoingCall
  to         : CallHierarchyItem
  fromRanges : List Range
%runElab deriveJSON defaultOpts `{CallHierarchyOutgoingCall}