text:
module Idris.Desugar

import Core.Binary
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Options
import Core.TT
import Core.Unify

import Data.StringMap
import Data.ANameMap

import Idris.DocString
import Idris.Syntax

import Idris.Elab.Implementation
import Idris.Elab.Interface

import Parser.Lexer.Source

import TTImp.BindImplicits
import TTImp.Parser
import TTImp.TTImp
import TTImp.Utils

import Utils.Shunting

import Control.Monad.State
import Data.List

-- Convert high level Idris declarations (PDecl from Idris.Syntax) into
-- TTImp, recording any high level syntax info on the way (e.g. infix
-- operators)

-- Desugaring from high level Idris syntax to TTImp involves:

-- * Shunting infix operators into function applications according to precedence
-- * Replacing 'do' notating with applications of (>>=)
-- * Replacing pattern matching binds with 'case'
-- * Changing tuples to 'Pair/MkPair'
-- * List notation
-- * Replacing !-notation
-- * Dependent pair notation
-- * Idiom brackets

%default covering

public export
data Side = LHS | AnyExpr

ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e

export
extendSyn : {auto s : Ref Syn SyntaxInfo} ->
            SyntaxInfo -> Core ()
extendSyn newsyn
    = do syn <- get Syn
         put Syn (record { infixes $= mergeLeft (infixes newsyn),
                           prefixes $= mergeLeft (prefixes newsyn),
                           ifaces $= merge (ifaces newsyn),
                           docstrings $= merge (docstrings newsyn),
                           bracketholes $= ((bracketholes newsyn) ++) }
                  syn)

mkPrec : Fixity -> Nat -> OpPrec
mkPrec InfixL p = AssocL p
mkPrec InfixR p = AssocR p
mkPrec Infix p = NonAssoc p
mkPrec Prefix p = Prefix p

toTokList : {auto s : Ref Syn SyntaxInfo} ->
            PTerm -> Core (List (Tok OpStr PTerm))
toTokList (POp fc opn l r)
    = do syn <- get Syn
         let op = nameRoot opn
         case lookup op (infixes syn) of
              Nothing =>
                  if any isOpChar (unpack op)
                     then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
                     else do rtoks <- toTokList r
                             pure (Expr l :: Op fc opn backtickPrec :: rtoks)
              Just (Prefix, _) =>
                      throw (GenericMsg fc $ "'" ++ op ++ "' is a prefix operator")
              Just (fix, prec) =>
                   do rtoks <- toTokList r
                      pure (Expr l :: Op fc opn (mkPrec fix prec) :: rtoks)
  where
    backtickPrec : OpPrec
    backtickPrec = NonAssoc 1
toTokList (PPrefixOp fc opn arg)
    = do syn <- get Syn
         let op = nameRoot opn
         case lookup op (prefixes syn) of
              Nothing =>
                   throw (GenericMsg fc $ "'" ++ op ++ "' is not a prefix operator")
              Just prec =>
                   do rtoks <- toTokList arg
                      pure (Op fc opn (Prefix prec) :: rtoks)
toTokList t = pure [Expr t]

record BangData where
  constructor MkBangData
  nextName : Int
  bangNames : List (Name, FC, RawImp)

initBangs : BangData
initBangs = MkBangData 0 []

bindBangs : List (Name, FC, RawImp) -> RawImp -> RawImp
bindBangs [] tm = tm
bindBangs ((n, fc, btm) :: bs) tm
    = bindBangs bs $ IApp fc (IApp fc (IVar fc (UN ">>=")) btm)
                          (ILam fc top Explicit (Just n)
                                (Implicit fc False) tm)

idiomise : FC -> RawImp -> RawImp
idiomise fc (IApp afc f a)
    = IApp fc (IApp fc (IVar fc (UN "<*>"))
                    (idiomise afc f))
                    a
idiomise fc fn = IApp fc (IVar fc (UN "pure")) fn

pairname : Name
pairname = NS builtinNS (UN "Pair")

mkpairname : Name
mkpairname = NS builtinNS (UN "MkPair")

dpairname : Name
dpairname = NS dpairNS (UN "DPair")

mkdpairname : Name
mkdpairname = NS dpairNS (UN "MkDPair")

data Bang : Type where

mutual
  desugarB : {auto s : Ref Syn SyntaxInfo} ->
             {auto b : Ref Bang BangData} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             Side -> List Name -> PTerm -> Core RawImp
  desugarB side ps (PRef fc x) = pure $ IVar fc x
  desugarB side ps (PPi fc rig p mn argTy retTy)
      = let ps' = maybe ps (:: ps) mn in
            pure $ IPi fc rig !(traverse (desugar side ps') p)
                              mn !(desugarB side ps argTy)
                                 !(desugarB side ps' retTy)
  desugarB side ps (PLam fc rig p (PRef _ n@(UN _)) argTy scope)
      = pure $ ILam fc rig !(traverse (desugar side ps) p)
                           (Just n) !(desugarB side ps argTy)
                                    !(desugar side (n :: ps) scope)
  desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
      = pure $ ILam fc rig !(traverse (desugar side ps) p)
                           (Just n) !(desugarB side ps argTy)
                                    !(desugar side (n :: ps) scope)
  desugarB side ps (PLam fc rig p (PImplicit _) argTy scope)
      = pure $ ILam fc rig !(traverse (desugar side ps) p)
                           Nothing !(desugarB side ps argTy)
                                   !(desugar side ps scope)
  desugarB side ps (PLam fc rig p pat argTy scope)
      = pure $ ILam fc rig !(traverse (desugar side ps) p)
                   (Just (MN "lamc" 0)) !(desugarB side ps argTy) $
                 ICase fc (IVar fc (MN "lamc" 0)) (Implicit fc False)
                     [!(desugarClause ps True (MkPatClause fc pat scope []))]
  desugarB side ps (PLet fc rig (PRef _ n) nTy nVal scope [])
      = pure $ ILet fc rig n !(desugarB side ps nTy) !(desugarB side ps nVal)
                             !(desugar side (n :: ps) scope)
  desugarB side ps (PLet fc rig pat nTy nVal scope alts)
      = pure $ ICase fc !(desugarB side ps nVal) !(desugarB side ps nTy)
                        !(traverse (desugarClause ps True)
                            (MkPatClause fc pat scope [] :: alts))
  desugarB side ps (PCase fc x xs)
      = pure $ ICase fc !(desugarB side ps x)
                        (Implicit fc False)
                        !(traverse (desugarClause ps True) xs)
  desugarB side ps (PLocal fc xs scope)
      = let ps' = definedIn xs ++ ps in
            pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs))
                             !(desugar side ps' scope)
  desugarB side ps (PApp pfc (PUpdate fc fs) rec)
      = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
                           !(desugarB side ps rec)
  desugarB side ps (PUpdate fc fs)
      = desugarB side ps (PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc)
                            (PApp fc (PUpdate fc fs) (PRef fc (MN "rec" 0))))
  desugarB side ps (PApp fc x y)
      = pure $ IApp fc !(desugarB side ps x) !(desugarB side ps y)
  desugarB side ps (PWithApp fc x y)
      = pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y)
  desugarB side ps (PImplicitApp fc x argn y)
      = pure $ IImplicitApp fc !(desugarB side ps x) argn !(desugarB side ps y)
  desugarB side ps (PDelayed fc r ty)
      = pure $ IDelayed fc r !(desugarB side ps ty)
  desugarB side ps (PDelay fc tm)
      = pure $ IDelay fc !(desugarB side ps tm)
  desugarB side ps (PForce fc tm)
      = pure $ IForce fc !(desugarB side ps tm)
  desugarB side ps (PEq fc l r)
      = do l' <- desugarB side ps l
           r' <- desugarB side ps r
           pure $ IAlternative fc FirstSuccess
                     [apply (IVar fc (UN "===")) [l', r'],
                      apply (IVar fc (UN "~=~")) [l', r']]
  desugarB side ps (PBracketed fc e) = desugarB side ps e
  desugarB side ps (POp fc op l r)
      = do ts <- toTokList (POp fc op l r)
           desugarTree side ps !(parseOps ts)
  desugarB side ps (PPrefixOp fc op arg)
      = do ts <- toTokList (PPrefixOp fc op arg)
           desugarTree side ps !(parseOps ts)
  desugarB side ps (PSectionL fc op arg)
      = do syn <- get Syn
           -- It might actually be a prefix argument rather than a section
           -- so check that first, otherwise desugar as a lambda
           case lookup (nameRoot op) (prefixes syn) of
                Nothing =>
                   desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
                               (POp fc op (PRef fc (MN "arg" 0)) arg))
                Just prec => desugarB side ps (PPrefixOp fc op arg)
  desugarB side ps (PSectionR fc arg op)
      = desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
                 (POp fc op arg (PRef fc (MN "arg" 0))))
  desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth
  desugarB side ps (PPrimVal fc (BI x))
      = case !fromIntegerName of
             Nothing =>
                pure $ IAlternative fc (UniqueDefault (IPrimVal fc (BI x)))
                                [IPrimVal fc (BI x),
                                 IPrimVal fc (I (fromInteger x))]
             Just fi => pure $ IApp fc (IVar fc fi)
                                       (IPrimVal fc (BI x))
  desugarB side ps (PPrimVal fc (Str x))
      = case !fromStringName of
             Nothing =>
                pure $ IPrimVal fc (Str x)
             Just f => pure $ IApp fc (IVar fc f)
                                      (IPrimVal fc (Str x))
  desugarB side ps (PPrimVal fc (Ch x))
      = case !fromCharName of
             Nothing =>
                pure $ IPrimVal fc (Ch x)
             Just f => pure $ IApp fc (IVar fc f)
                                      (IPrimVal fc (Ch x))
  desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x
  desugarB side ps (PQuote fc tm)
      = pure $ IQuote fc !(desugarB side ps tm)
  desugarB side ps (PQuoteName fc n)
      = pure $ IQuoteName fc n
  desugarB side ps (PQuoteDecl fc x)
      = do xs <- traverse (desugarDecl ps) x
           pure $ IQuoteDecl fc (concat xs)
  desugarB side ps (PUnquote fc tm)
      = pure $ IUnquote fc !(desugarB side ps tm)
  desugarB side ps (PRunElab fc tm)
      = pure $ IRunElab fc !(desugarB side ps tm)
  desugarB side ps (PHole fc br holename)
      = do when br $
              do syn <- get Syn
                 put Syn (record { bracketholes $= ((UN holename) ::) } syn)
           pure $ IHole fc holename
  desugarB side ps (PType fc) = pure $ IType fc
  desugarB side ps (PAs fc vname pattern)
      = pure $ IAs fc UseRight vname !(desugarB side ps pattern)
  desugarB side ps (PDotted fc x)
      = pure $ IMustUnify fc UserDotted !(desugarB side ps x)
  desugarB side ps (PImplicit fc) = pure $ Implicit fc True
  desugarB side ps (PInfer fc) = pure $ Implicit fc False
  desugarB side ps (PDoBlock fc ns block)
      = expandDo side ps fc ns block
  desugarB side ps (PBang fc term)
      = do itm <- desugarB side ps term
           bs <- get Bang
           let bn = MN "bind" (nextName bs)
           put Bang (record { nextName $= (+1),
                              bangNames $= ((bn, fc, itm) ::)
                            } bs)
           pure (IVar fc bn)
  desugarB side ps (PIdiom fc term)
      = do itm <- desugarB side ps term
           pure (idiomise fc itm)
  desugarB side ps (PList fc args)
      = expandList side ps fc args
  desugarB side ps (PPair fc l r)
      = do l' <- desugarB side ps l
           r' <- desugarB side ps r
           let pval = apply (IVar fc mkpairname) [l', r']
           pure $ IAlternative fc (UniqueDefault pval)
                  [apply (IVar fc pairname) [l', r'], pval]
  desugarB side ps (PDPair fc (PRef nfc (UN n)) (PImplicit _) r)
      = do r' <- desugarB side ps r
           let pval = apply (IVar fc mkdpairname) [IVar nfc (UN n), r']
           pure $ IAlternative fc (UniqueDefault pval)
                  [apply (IVar fc dpairname)
                      [Implicit nfc False,
                       ILam nfc top Explicit (Just (UN n)) (Implicit nfc False) r'],
                   pval]
  desugarB side ps (PDPair fc (PRef nfc (UN n)) ty r)
      = do ty' <- desugarB side ps ty
           r' <- desugarB side ps r
           pure $ apply (IVar fc dpairname)
                        [ty',
                         ILam nfc top Explicit (Just (UN n)) ty' r']
  desugarB side ps (PDPair fc l (PImplicit _) r)
      = do l' <- desugarB side ps l
           r' <- desugarB side ps r
           pure $ apply (IVar fc mkdpairname) [l', r']
  desugarB side ps (PDPair fc l ty r)
      = throw (GenericMsg fc "Invalid dependent pair type")
  desugarB side ps (PUnit fc)
      = pure $ IAlternative fc (UniqueDefault (IVar fc (UN "MkUnit")))
               [IVar fc (UN "Unit"),
                IVar fc (UN "MkUnit")]
  desugarB side ps (PIfThenElse fc x t e)
      = pure $ ICase fc !(desugarB side ps x) (IVar fc (UN "Bool"))
                   [PatClause fc (IVar fc (UN "True")) !(desugar side ps t),
                    PatClause fc (IVar fc (UN "False")) !(desugar side ps e)]
  desugarB side ps (PComprehension fc ret conds)
      = desugarB side ps (PDoBlock fc Nothing (map guard conds ++ [toPure ret]))
    where
      guard : PDo -> PDo
      guard (DoExp fc tm) = DoExp fc (PApp fc (PRef fc (UN "guard")) tm)
      guard d = d

      toPure : PTerm -> PDo
      toPure tm = DoExp fc (PApp fc (PRef fc (UN "pure")) tm)
  desugarB side ps (PRewrite fc rule tm)
      = pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm)
  desugarB side ps (PRange fc start next end)
      = case next of
             Nothing =>
                desugarB side ps (PApp fc
                                    (PApp fc (PRef fc (UN "rangeFromTo"))
                                          start) end)
             Just n =>
                desugarB side ps (PApp fc
                                    (PApp fc
                                        (PApp fc (PRef fc (UN "rangeFromThenTo"))
                                              start) n) end)
  desugarB side ps (PRangeStream fc start next)
      = case next of
             Nothing =>
                desugarB side ps (PApp fc (PRef fc (UN "rangeFrom")) start)
             Just n =>
                desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
  desugarB side ps (PUnifyLog fc lvl tm)
      = pure $ IUnifyLog fc lvl !(desugarB side ps tm)

  desugarB side ps (PPostfixProjs fc rec projs)
      = do
        let isPRef = \case
              PRef _ _ => True
              _ => False
        defs <- get Ctxt
        when (not (isExtension PostfixProjections defs) && not (all isPRef projs)) $
          throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")

        desugarB side ps $ foldl (\x, proj => PApp fc proj x) rec projs

  desugarB side ps (PPostfixProjsSection fc projs args)
      = do
        let isPRef = \case
              PRef _ _ => True
              _ => False
        defs <- get Ctxt

        when (not (isExtension PostfixProjections defs)) $ do
          when (not (all isPRef projs)) $
            throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")

          case args of
            [] => pure ()
            _  => throw $ GenericMsg fc "postfix projection sections require %language PostfixProjections"

        desugarB side ps $
          PLam fc top Explicit (PRef fc (MN "paRoot" 0)) (PImplicit fc) $
            foldl
              (\r, arg => PApp fc r arg)
              (foldl
                (\r, proj => PApp fc proj r)
                (PRef fc (MN "paRoot" 0))
                projs)
              args

  desugarB side ps (PWithUnambigNames fc ns rhs)
      = IWithUnambigNames fc ns <$> desugarB side ps rhs

  desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
                  {auto b : Ref Bang BangData} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  {auto m : Ref MD Metadata} ->
                  Side -> List Name -> PFieldUpdate -> Core IFieldUpdate
  desugarUpdate side ps (PSetField p v)
      = pure (ISetField p !(desugarB side ps v))
  desugarUpdate side ps (PSetFieldApp p v)
      = pure (ISetFieldApp p !(desugarB side ps v))

  expandList : {auto s : Ref Syn SyntaxInfo} ->
               {auto b : Ref Bang BangData} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto m : Ref MD Metadata} ->
               Side -> List Name -> FC -> List PTerm -> Core RawImp
  expandList side ps fc [] = pure (IVar fc (UN "Nil"))
  expandList side ps fc (x :: xs)
      = pure $ apply (IVar fc (UN "::"))
                [!(desugarB side ps x), !(expandList side ps fc xs)]

  addNS : Maybe Namespace -> Name -> Name
  addNS (Just ns) n@(NS _ _) = n
  addNS (Just ns) n = NS ns n
  addNS _ n = n

  expandDo : {auto s : Ref Syn SyntaxInfo} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto m : Ref MD Metadata} ->
             Side -> List Name -> FC -> Maybe Namespace -> List PDo -> Core RawImp
  expandDo side ps fc ns [] = throw (GenericMsg fc "Do block cannot be empty")
  expandDo side ps _ _ [DoExp fc tm] = desugar side ps tm
  expandDo side ps fc ns [e]
      = throw (GenericMsg (getLoc e)
                  "Last statement in do block must be an expression")
  expandDo side ps topfc ns (DoExp fc tm :: rest)
      = do tm' <- desugar side ps tm
           rest' <- expandDo side ps topfc ns rest
           -- A free standing 'case' block must return ()
           let ty = case tm' of
                         ICase _ _ _ _ => IVar fc (UN "Unit")
                         _ => Implicit fc False
           gam <- get Ctxt
           pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) tm')
                          (ILam fc top Explicit Nothing
                                ty rest')
  expandDo side ps topfc ns (DoBind fc n tm :: rest)
      = do tm' <- desugar side ps tm
           rest' <- expandDo side ps topfc ns rest
           pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) tm')
                     (ILam fc top Explicit (Just n)
                           (Implicit fc False) rest')
  expandDo side ps topfc ns (DoBindPat fc pat exp alts :: rest)
      = do pat' <- desugar LHS ps pat
           (newps, bpat) <- bindNames False pat'
           exp' <- desugar side ps exp
           alts' <- traverse (desugarClause ps True) alts
           let ps' = newps ++ ps
           rest' <- expandDo side ps' topfc ns rest
           pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) exp')
                    (ILam fc top Explicit (Just (MN "_" 0))
                          (Implicit fc False)
                          (ICase fc (IVar fc (MN "_" 0))
                               (Implicit fc False)
                               (PatClause fc bpat rest'
                                  :: alts')))
  expandDo side ps topfc ns (DoLet fc n rig ty tm :: rest)
      = do b <- newRef Bang initBangs
           tm' <- desugarB side ps tm
           ty' <- desugar side ps ty
           rest' <- expandDo side ps topfc ns rest
           let bind = ILet fc rig n ty' tm' rest'
           bd <- get Bang
           pure $ bindBangs (bangNames bd) bind
  expandDo side ps topfc ns (DoLetPat fc pat ty tm alts :: rest)
      = do b <- newRef Bang initBangs
           pat' <- desugar LHS ps pat
           ty' <- desugar side ps ty
           (newps, bpat) <- bindNames False pat'
           tm' <- desugarB side ps tm
           alts' <- traverse (desugarClause ps True) alts
           let ps' = newps ++ ps
           rest' <- expandDo side ps' topfc ns rest
           bd <- get Bang
           pure $ bindBangs (bangNames bd) $
                    ICase fc tm' ty'
                       (PatClause fc bpat rest'
                                  :: alts')
  expandDo side ps topfc ns (DoLetLocal fc decls :: rest)
      = do rest' <- expandDo side ps topfc ns rest
           decls' <- traverse (desugarDecl ps) decls
           pure $ ILocal fc (concat decls') rest'
  expandDo side ps topfc ns (DoRewrite fc rule :: rest)
      = do rest' <- expandDo side ps topfc ns rest
           rule' <- desugar side ps rule
           pure $ IRewrite fc rule' rest'

  desugarTree : {auto s : Ref Syn SyntaxInfo} ->
                {auto b : Ref Bang BangData} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                Side -> List Name -> Tree OpStr PTerm -> Core RawImp
  desugarTree side ps (Infix loc (UN "=") l r) -- special case since '=' is special syntax
      = do l' <- desugarTree side ps l
           r' <- desugarTree side ps r
           pure (IAlternative loc FirstSuccess
                     [apply (IVar loc (UN "===")) [l', r'],
                      apply (IVar loc (UN "~=~")) [l', r']])
  desugarTree side ps (Infix loc (UN "$") l r) -- special case since '$' is special syntax
      = do l' <- desugarTree side ps l
           r' <- desugarTree side ps r
           pure (IApp loc l' r')
  desugarTree side ps (Infix loc op l r)
      = do l' <- desugarTree side ps l
           r' <- desugarTree side ps r
           pure (IApp loc (IApp loc (IVar loc op) l') r')
  -- negation is a special case, since we can't have an operator with
  -- two meanings otherwise
  desugarTree side ps (Pre loc (UN "-") arg)
      = do arg' <- desugarTree side ps arg
           pure (IApp loc (IVar loc (UN "negate")) arg')
  desugarTree side ps (Pre loc op arg)
      = do arg' <- desugarTree side ps arg
           pure (IApp loc (IVar loc op) arg')
  desugarTree side ps (Leaf t) = desugarB side ps t

  desugarType : {auto s : Ref Syn SyntaxInfo} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                List Name -> PTypeDecl -> Core ImpTy
  desugarType ps (MkPTy fc n d ty)
      = do addDocString n d
           syn <- get Syn
           pure $ MkImpTy fc n !(bindTypeNames (usingImpl syn)
                                               ps !(desugar AnyExpr ps ty))

  desugarClause : {auto s : Ref Syn SyntaxInfo} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  {auto m : Ref MD Metadata} ->
                  List Name -> Bool -> PClause -> Core ImpClause
  desugarClause ps arg (MkPatClause fc lhs rhs wheres)
      = do ws <- traverse (desugarDecl ps) wheres
           (bound, blhs) <- bindNames arg !(desugar LHS ps lhs)
           rhs' <- desugar AnyExpr (bound ++ ps) rhs
           pure $ PatClause fc blhs
                     (case ws of
                           [] => rhs'
                           _ => ILocal fc (concat ws) rhs')
  desugarClause ps arg (MkWithClause fc lhs wval flags cs)
      = do cs' <- traverse (desugarClause ps arg) cs
           (bound, blhs) <- bindNames arg !(desugar LHS ps lhs)
           wval' <- desugar AnyExpr (bound ++ ps) wval
           pure $ WithClause fc blhs wval' flags cs'
  desugarClause ps arg (MkImpossible fc lhs)
      = do dlhs <- desugar LHS ps lhs
           pure $ ImpossibleClause fc (snd !(bindNames arg dlhs))

  desugarData : {auto s : Ref Syn SyntaxInfo} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                List Name -> (doc : String) ->
                PDataDecl -> Core ImpData
  desugarData ps doc (MkPData fc n tycon opts datacons)
      = do addDocString n doc
           syn <- get Syn
           pure $ MkImpData fc n
                              !(bindTypeNames (usingImpl syn)
                                              ps !(desugar AnyExpr ps tycon))
                              opts
                              !(traverse (desugarType ps) datacons)
  desugarData ps doc (MkPLater fc n tycon)
      = do addDocString n doc
           syn <- get Syn
           pure $ MkImpLater fc n !(bindTypeNames (usingImpl syn)
                                                  ps !(desugar AnyExpr ps tycon))

  desugarField : {auto s : Ref Syn SyntaxInfo} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 {auto m : Ref MD Metadata} ->
                 List Name -> Namespace -> PField ->
                 Core IField
  desugarField ps ns (MkField fc doc rig p n ty)
      = do addDocStringNS ns n doc
           syn <- get Syn
           pure (MkIField fc rig !(traverse (desugar AnyExpr ps) p )
                          n !(bindTypeNames (usingImpl syn)
                          ps !(desugar AnyExpr ps ty)))

  -- Get the declaration to process on each pass of a mutual block
  -- Essentially: types on the first pass
  --    i.e. type constructors of data declarations
  --         function types
  --         interfaces (in full, since it includes function types)
  --         records (just the generated type constructor)
  --         implementation headers (i.e. note their existence, but not the bodies)
  -- Everything else on the second pass
  getDecl : Pass -> PDecl -> Maybe PDecl
  getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds)
      = Just (PImplementation fc vis opts p is cons n ps iname nusing ds)

  getDecl p (PNamespace fc ns ds)
      = Just (PNamespace fc ns (mapMaybe (getDecl p) ds))

  getDecl AsType d@(PClaim _ _ _ _ _) = Just d
  getDecl AsType (PData fc doc vis (MkPData dfc tyn tyc _ _))
      = Just (PData fc doc vis (MkPLater dfc tyn tyc))
  getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d
  getDecl AsType d@(PRecord fc doc vis n ps _ _)
      = Just (PData fc doc vis (MkPLater fc n (mkRecType ps)))
    where
      mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm
      mkRecType [] = PType fc
      mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts)
  getDecl AsType d@(PFixity _ _ _ _) = Just d
  getDecl AsType d@(PDirective _ _) = Just d
  getDecl AsType d = Nothing

  getDecl AsDef (PClaim _ _ _ _ _) = Nothing
  getDecl AsDef d@(PData _ _ _ (MkPLater _ _ _)) = Just d
  getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing
  getDecl AsDef d@(PRecord _ _ _ _ _ _ _) = Just d
  getDecl AsDef (PFixity _ _ _ _) = Nothing
  getDecl AsDef (PDirective _ _) = Nothing
  getDecl AsDef d = Just d

  getDecl p (PParameters fc ps pds)
      = Just (PParameters fc ps (mapMaybe (getDecl p) pds))
  getDecl p (PUsing fc ps pds)
      = Just (PUsing fc ps (mapMaybe (getDecl p) pds))

  getDecl Single d = Just d

  export
  desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 {auto m : Ref MD Metadata} ->
                 List Name -> PFnOpt -> Core FnOpt
  desugarFnOpt ps (IFnOpt f) = pure f
  desugarFnOpt ps (PForeign tms)
      = do tms' <- traverse (desugar AnyExpr ps) tms
           pure (ForeignFn tms')

  -- Given a high level declaration, return a list of TTImp declarations
  -- which process it, and update any necessary state on the way.
  export
  desugarDecl : {auto s : Ref Syn SyntaxInfo} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                List Name -> PDecl -> Core (List ImpDecl)
  desugarDecl ps (PClaim fc rig vis fnopts ty)
      = do opts <- traverse (desugarFnOpt ps) fnopts
           pure [IClaim fc rig vis opts !(desugarType ps ty)]
        where
          isTotalityOption : FnOpt -> Bool
          isTotalityOption (Totality _) = True
          isTotalityOption _            = False

  desugarDecl ps (PDef fc clauses)
  -- The clauses won't necessarily all be from the same function, so split
  -- after desugaring, by function name, using collectDefs from RawImp
      = do cs <- traverse (desugarClause ps False) clauses
           defs <- traverse toIDef cs
           pure (collectDefs defs)
    where
      getFn : RawImp -> Core Name
      getFn (IVar _ n) = pure n
      getFn (IApp _ f _) = getFn f
      getFn (IImplicitApp _ f _ _) = getFn f
      getFn tm = throw (InternalError (show tm ++ " is not a function application"))

      toIDef : ImpClause -> Core ImpDecl
      toIDef (PatClause fc lhs rhs)
          = pure $ IDef fc !(getFn lhs) [PatClause fc lhs rhs]
      toIDef (WithClause fc lhs rhs flags cs)
          = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs flags cs]
      toIDef (ImpossibleClause fc lhs)
          = pure $ IDef fc !(getFn lhs) [ImpossibleClause fc lhs]

  desugarDecl ps (PData fc doc vis ddecl)
      = pure [IData fc vis !(desugarData ps doc ddecl)]
  desugarDecl ps (PParameters fc params pds)
      = do pds' <- traverse (desugarDecl (ps ++ map fst params)) pds
           params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
                                            pure (fst ntm, tm')) params
           -- Look for implicitly bindable names in the parameters
           let pnames = ifThenElse !isUnboundImplicits
                          (concatMap (findBindableNames True
                                         (ps ++ map Builtin.fst params) [])
                                       (map Builtin.snd params'))
                          []
           let paramsb = map (\ ntm => (Builtin.fst ntm,
                                        doBind pnames (Builtin.snd ntm))) params'
           pure [IParameters fc paramsb (concat pds')]
  desugarDecl ps (PUsing fc uimpls uds)
      = do syn <- get Syn
           let oldu = usingImpl syn
           uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
                                            btm <- bindTypeNames oldu ps tm'
                                            pure (fst ntm, btm)) uimpls
           put Syn (record { usingImpl = uimpls' ++ oldu } syn)
           uds' <- traverse (desugarDecl ps) uds
           syn <- get Syn
           put Syn (record { usingImpl = oldu } syn)
           pure (concat uds')
  desugarDecl ps (PReflect fc tm)
      = throw (GenericMsg fc "Reflection not implemented yet")
--       pure [IReflect fc !(desugar AnyExpr ps tm)]
  desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
      = do addDocString tn doc
           let cons = concatMap expandConstraint cons_in
           cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ map fst params)
                                                         (snd ntm)
                                          pure (fst ntm, tm')) cons
           params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
                                            pure (fst ntm, tm')) params
           -- Look for bindable names in all the constraints and parameters
           let mnames = map dropNS (definedIn body)
           let bnames = ifThenElse !isUnboundImplicits
                          (concatMap (findBindableNames True
                                      (ps ++ mnames ++ map fst params) [])
                                  (map Builtin.snd cons') ++
                           concatMap (findBindableNames True
                                      (ps ++ mnames ++ map fst params) [])
                                  (map Builtin.snd params'))
                          []
           let paramsb = map (\ ntm => (Builtin.fst ntm,
                                        doBind bnames (Builtin.snd ntm))) params'
           let consb = map (\ ntm => (Builtin.fst ntm,
                                      doBind bnames (Builtin.snd ntm))) cons'

           body' <- traverse (desugarDecl (ps ++ mnames ++ map fst params)) body
           pure [IPragma (\nest, env =>
                             elabInterface fc vis env nest consb
                                           tn paramsb det conname
                                           (concat body'))]
    where
      -- Turns pairs in the constraints to individual constraints. This
      -- is a bit of a hack, but it's necessary to build parent constraint
      -- chasing functions correctly
      pairToCons : PTerm -> List PTerm
      pairToCons (PPair _ l r) = pairToCons l ++ pairToCons r
      pairToCons t = [t]

      expandConstraint : (Maybe Name, PTerm) -> List (Maybe Name, PTerm)
      expandConstraint (Just n, t) = [(Just n, t)]
      expandConstraint (Nothing, p)
          = map (\x => (Nothing, x)) (pairToCons p)

  desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impname nusing body)
      = do opts <- traverse (desugarFnOpt ps) fnopts
           is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
                                             pure (n, c, tm')) is
           let _ = the (List (Name, RigCount, RawImp)) is'
           cons' <- traverse (\ (n, tm) => do tm' <- desugar AnyExpr ps tm
                                              pure (n, tm')) cons
           let _ = the (List (Maybe Name, RawImp)) cons'
           params' <- traverse (desugar AnyExpr ps) params
           let _ = the (List RawImp) params'
           -- Look for bindable names in all the constraints and parameters
           let bnames = if !isUnboundImplicits
                        then
                        concatMap (findBindableNames True ps []) (map snd cons') ++
                        concatMap (findBindableNames True ps []) params'
                        else []

           let paramsb = map (doBind bnames) params'
           let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is'
           let _ = the (List (Name, RigCount, RawImp)) isb
           let consb = map (\(n, tm) => (n, doBind bnames tm)) cons'
           let _ = the (List (Maybe Name, RawImp)) consb

           body' <- maybe (pure Nothing)
                          (\b => do b' <- traverse (desugarDecl ps) b
                                    pure (Just (concat b'))) body
           pure [IPragma (\nest, env =>
                             elabImplementation fc vis opts pass env nest isb consb
                                                tn paramsb impname nusing
                                                body')]

  desugarDecl ps (PRecord fc doc vis tn params conname_in fields)
      = do addDocString tn doc
           params' <- traverse (\ (n,c,p,tm) =>
                          do tm' <- desugar AnyExpr ps tm
                             p'  <- mapDesugarPiInfo ps p
                             pure (n, c, p', tm'))
                        params
           let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) params'
           let fnames = map fname fields
           let _ = the (List Name) fnames
           -- Look for bindable names in the parameters

           let bnames = if !isUnboundImplicits
                        then concatMap (findBindableNames True
                                         (ps ++ fnames ++ map fst params) [])
                                       (map (\(_,_,_,d) => d) params')
                        else []
           let _ = the (List (String, String)) bnames

           let paramsb = map (\ (n, c, p, tm) => (n, c, p, doBind bnames tm)) params'
           let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) paramsb
           let recName = nameRoot tn
           fields' <- traverse (desugarField (ps ++ map fname fields ++
                                              map fst params) (mkNamespace recName))
                               fields
           let _ = the (List IField) fields'
           let conname = maybe (mkConName tn) id conname_in
           let _ = the Name conname
           pure [IRecord fc (Just recName)
                         vis (MkImpRecord fc tn paramsb conname fields')]
    where
      fname : PField -> Name
      fname (MkField _ _ _ _ n _) = n

      mkConName : Name -> Name
      mkConName (NS ns (UN n)) = NS ns (DN n (MN ("__mk" ++ n) 0))
      mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)

      mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
      mapDesugarPiInfo ps Implicit         = pure   Implicit
      mapDesugarPiInfo ps Explicit         = pure   Explicit
      mapDesugarPiInfo ps AutoImplicit     = pure   AutoImplicit
      mapDesugarPiInfo ps (DefImplicit tm) = pure $ DefImplicit
                                                  !(desugar AnyExpr ps tm)

  desugarDecl ps (PFixity fc Prefix prec (UN n))
      = do syn <- get Syn
           put Syn (record { prefixes $= insert n prec } syn)
           pure []
  desugarDecl ps (PFixity fc fix prec (UN n))
      = do syn <- get Syn
           put Syn (record { infixes $= insert n (fix, prec) } syn)
           pure []
  desugarDecl ps (PFixity fc _ _ _)
      = throw (GenericMsg fc "Fixity declarations must be for unqualified names")
  desugarDecl ps (PMutual fc ds)
      = do let mds = mapMaybe (getDecl AsType) ds ++ mapMaybe (getDecl AsDef) ds
           mds' <- traverse (desugarDecl ps) mds
           pure (concat mds')
  desugarDecl ps (PNamespace fc ns decls)
      = do ds <- traverse (desugarDecl ps) decls
           pure [INamespace fc ns (concat ds)]
  desugarDecl ps (PTransform fc n lhs rhs)
      = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
           rhs' <- desugar AnyExpr (bound ++ ps) rhs
           pure [ITransform fc (UN n) blhs rhs']
  desugarDecl ps (PRunElabDecl fc tm)
      = do tm' <- desugar AnyExpr ps tm
           pure [IRunElabDecl fc tm']
  desugarDecl ps (PDirective fc d)
      = case d of
             Hide n => pure [IPragma (\nest, env => hide fc n)]
             Logging i => pure [ILog (topics i, verbosity i)]
             LazyOn a => pure [IPragma (\nest, env => lazyActive a)]
             UnboundImplicits a => do
               setUnboundImplicits a
               pure [IPragma (\nest, env => setUnboundImplicits a)]
             AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
             AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
             PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]
             RewriteName eq rw => pure [IPragma (\nest, env => setRewrite fc eq rw)]
             PrimInteger n => pure [IPragma (\nest, env => setFromInteger n)]
             PrimString n => pure [IPragma (\nest, env => setFromString n)]
             PrimChar n => pure [IPragma (\nest, env => setFromChar n)]
             CGAction cg dir => pure [IPragma (\nest, env => addDirective cg dir)]
             Names n ns => pure [IPragma (\nest, env => addNameDirective fc n ns)]
             StartExpr tm => pure [IPragma (\nest, env => throw (InternalError "%start not implemented"))] -- TODO!
             Overloadable n => pure [IPragma (\nest, env => setNameFlag fc n Overloadable)]
             Extension e => pure [IPragma (\nest, env => setExtension e)]
             DefaultTotality tot => pure [IPragma (\_, _ => setDefaultTotalityOption tot)]

  export
  desugar : {auto s : Ref Syn SyntaxInfo} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            Side -> List Name -> PTerm -> Core RawImp
  desugar s ps tm
      = do b <- newRef Bang initBangs
           tm' <- desugarB s ps tm
           bd <- get Bang
           pure $ bindBangs (bangNames bd) tm'


text:
module Flexidisc.RecordContent

import Control.Monad.Identity
import Flexidisc.OrdList
import Flexidisc.TaggedValue
import Flexidisc.THList

%default total
%access export

public export
OrdHeader : (k : Type) -> (o : Ord k) -> Type
OrdHeader k o = OrdList k o Type

public export
data RecordContentM : (m : Type -> Type) ->
                      (k : Type) -> (o : Ord k) -> (OrdHeader k o) -> Type where
  Nil  : RecordContentM m k o []
  (::) : TaggedValue k' (m a) -> RecordContentM m k o xs ->
         RecordContentM m k o ((k', a) :: xs)

cons : TaggedValue k' (m a) -> RecordContentM m k o xs ->
       RecordContentM m k o ((k', a) :: xs)
cons = (::)

%name RecordContentM xs, ys, zs

public export
RecordContent : (k : Type) -> (o : Ord k) -> (OrdHeader k o) -> Type
RecordContent = RecordContentM id

empty : RecordContentM m k o []
empty = Nil

insert : TaggedValue k' (m a) -> RecordContentM m k o header ->
         RecordContentM m k o (insert (k', a) header)
insert x [] = [x]
insert (k' := v) ((kx := vx) :: xs') with (k' < kx)
  | False = (kx := vx) :: (insert (k' := v) xs')
  | True  = (k' := v) :: (kx := vx) :: xs'

atLabel : RecordContentM m k o header -> (loc : OrdLabel l header) ->
          m (atLabel header loc)
atLabel ((l := x) :: _) Here      = x
atLabel (_ :: xs) (There later) = atLabel xs later

atRow : RecordContentM m k o header -> (loc : OrdRow l ty header) -> m ty
atRow ((l := x) :: _) Here      = x
atRow (_ :: xs) (There later) = atRow xs later

update : RecordContentM m k o header -> (loc : OrdRow l a header) ->
         (f : m a -> m b) ->
         RecordContentM m k o (changeValue header loc b)
update ((l := x) :: xs) Here f = (l := f x) :: xs
update (x :: xs) (There later) f = x :: update xs later f

set : RecordContentM m k o header ->
      (loc : OrdLabel l header) -> (new : m ty) ->
      RecordContentM m k o (changeValue header loc ty)
set ((l := x) :: xs) Here          new = (l := new) :: xs
set (x :: xs)        (There later) new = x          :: set xs later new

setByRow : RecordContentM m k o header ->
           (loc : OrdRow l tOld header) -> (new : m tNew) ->
           RecordContentM m k o (changeValue header loc tNew)
setByRow xs loc new = update xs loc (const new)

merge : (xs : RecordContentM m k o header) ->
        (ys : RecordContentM m k o header') ->
        RecordContentM m k o (merge header header')
merge [] ys = ys
merge (x :: zs) [] = x :: zs
merge ((k := x) :: zs) ((k' := y) :: ys) with (k < k')
  | True  = (k  := x) :: (merge zs ((k' := y) :: ys))
  | False = (k' := y) :: (merge ((k := x) :: zs) ys)

diff : DecEq k =>
       (xs : RecordContentM m k o header) ->
       (ys : RecordContentM m k o header') ->
       RecordContentM m k o (diffKeys header header')
diff [] ys = []
diff (kx := vx :: xs) ys {header'} with (decFresh kx header')
  | (Yes prf) = kx := vx :: diff xs ys
  | (No contra) = diff xs ys

infixl 7 |>

(|>) : DecEq k =>
       (xs : RecordContentM m k o header) ->
       (ys : RecordContentM m k o header') ->
       RecordContentM m k o (patch header header')
(|>) xs ys = merge (diff ys xs) xs

drop : RecordContentM m k o header -> (loc : OrdLabel l header) ->
       RecordContentM m k o (dropLabel header loc)
drop (_ :: xs) Here = xs
drop (x :: xs) (There later) = x :: drop xs later

project : RecordContentM m k o header -> Sub sub header ->
          RecordContentM m k o sub
project [] Empty = []
project (_ :: ys) (Skip sub) = project ys sub
project (x :: ys) (Keep sub) = x :: project ys sub

keep : (xs : RecordContentM m k o pre) -> (sub : SubWithKeys keys post pre) ->
       RecordContentM m k o post
keep xs = project xs . toSub

discard : (xs : RecordContentM m k o pre) ->
          (sub : CompWithKeys keys post pre) ->
          RecordContentM m k o post
discard xs = project xs . toSub

hoist : (f: {a : _} -> m a -> n a) -> RecordContentM m k o header ->
        RecordContentM n k o header
hoist f [] = []
hoist f (l := v :: xs) = (l := f v) :: hoist f xs

lift : (f : {a : _} -> a -> m a) -> RecordContent k o header ->
        RecordContentM m k o header
lift = hoist

unlift : RecordContentM m k o header -> RecordContent k o (map m header)
unlift [] = []
unlift (x :: ys) = x :: unlift ys

optional : (xs : RecordContent k o pre) -> (opt : HereOrNot post pre) ->
           RecordContentM Maybe k o post
optional [] Empty = []
optional xs (Skip compat yes) = _ := Nothing :: optional xs compat
optional (x :: xs) (Extra compat yes) = optional xs compat
optional (l := v :: xs) (Keep compat) = l := Just v :: optional xs compat

toTHList : RecordContentM m k o header -> THList m k (toList header)
toTHList [] = []
toTHList ((_ := x) :: xs) = x :: toTHList xs

sequence : Applicative m =>
           RecordContentM m k o header -> m (RecordContent k o header)
sequence [] = pure []
sequence ((k' := x) :: xs) = (map (cons . (k' :=)) x) <*> (sequence xs)

implementation Eq (RecordContentM m k o []) where
  (==) x y = True
  (/=) x y = False

implementation
(Eq (m t), Eq (RecordContentM m k o ts)) => Eq (RecordContentM m k o ((l,t) :: ts)) where
  (==) ((_ := x) :: xs) ((_ := y) :: ys) = x == y && xs == ys
  (/=) ((_ := x) :: xs) ((_ := y) :: ys) = x /= y || xs /= ys

ext: idr

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Foreign.Neovim.Loop

import public System.FFI.Lua

%default total

export
data Stream : Type where
  MkStream : OpaqueDict -> Stream

%foreign "function(_) return vim.loop.new_pipe(false) end"
prim__newPipe : PrimIO OpaqueDict

export
newPipe : HasIO io => io Stream
newPipe = MkStream <$> primIO prim__newPipe

export
data Socket : Type where
  MkSocket : OpaqueDict -> Socket

%foreign "function(_) return vim.loop.new_tcp() end"
prim__newTCP : PrimIO OpaqueDict

export
newTCP : HasIO io => io Socket
newTCP = MkSocket <$> primIO prim__newTCP

prim__spawn__ffi : String
prim__spawn__ffi =
    "function(cmd)"
 ++ "    return function(opts)"
 ++ "        return function (callback)"
 ++ "           return function (_)"
 ++ "               return vim.loop.spawn(cmd, opts, vim.schedule_wrap(idris.world(callback, 2)))"
 ++ "           end"
 ++ "        end"
 ++ "    end"
 ++ "end"

-- TODO: leave schedule_wrap here or generalise even more?
%foreign prim__spawn__ffi
prim__spawn : String -> OpaqueDict -> (Int -> Int -> PrimIO ()) -> PrimIO OpaqueDict

export
spawn : HasIO io
     => String
     -> Dict [("args", Lua.List [String, String]), ("stdio", Lua.List [OpaqueDict, OpaqueDict, OpaqueDict])]
     -> (Int -> Int -> IO ())
     -> io (Dict [("handle", OpaqueDict), ("pid", Int)])
spawn cmd (MkDict opts) f = MkDict <$> primIO (prim__spawn cmd opts (\x, y => toPrim $ f x y))


text:
module Core.SchemeEval.Evaluate

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.SchemeEval.Compile
import Core.SchemeEval.ToScheme
import Core.TT

import Libraries.Data.NameMap
import Libraries.Utils.Scheme

public export
data SObj : List Name -> Type where
     MkSObj : ForeignObj -> SchVars vars -> SObj vars

-- Values, which we read off evaluated scheme objects.
-- Unfortunately we can't quite get away with using Core.Value.NF because
-- of the different representation of closures. Also, we're call by value
-- when going via scheme, so this structure is a little bit simpler (not
-- recording a LocalEnv for example).
mutual
  public export
  data SHead : List Name -> Type where
       SLocal : (idx : Nat) -> (0 p : IsVar nm idx vars) -> SHead vars
       SRef : NameType -> Name -> SHead vars
       SMeta : Name -> Int -> List (Core (SNF vars)) -> SHead vars

  public export
  data SNF : List Name -> Type where
       SBind    : FC -> (x : Name) -> Binder (SNF vars) ->
                  (SObj vars -> Core (SNF vars)) -> SNF vars
       SApp     : FC -> SHead vars -> List (Core (SNF vars)) -> SNF vars
       SDCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->
                  List (Core (SNF vars)) -> SNF vars
       STCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->
                  List (Core (SNF vars)) -> SNF vars
       SDelayed : FC -> LazyReason -> SNF vars -> SNF vars
       SDelay   : FC -> LazyReason -> Core (SNF vars) -> Core (SNF vars) ->
                  SNF vars
       SForce   : FC -> LazyReason -> SNF vars -> SNF vars
       SPrimVal : FC -> Constant -> SNF vars
       SErased  : FC -> (imp : Bool) -> SNF vars
       SType    : FC -> Name -> SNF vars

getAllNames : {auto c : Ref Ctxt Defs} ->
              NameMap () -> List Name -> Core (NameMap ())
getAllNames done [] = pure done
getAllNames done (x :: xs)
    = do let Nothing = lookup x done
             | _ => getAllNames done xs
         defs <- get Ctxt
         Just gdef <- lookupCtxtExact x (gamma defs)
             | _ => getAllNames done xs
         getAllNames (insert x () done) (xs ++ keys (refersTo gdef))

-- Evaluate a term via scheme. This will throw if the backend doesn't
-- support scheme evaluation, so callers should have checked first and fall
-- back to the internal (slow!) evaluator if initialisation fails.
export
seval : {auto c : Ref Ctxt Defs} ->
        SchemeMode -> Env Term vars -> Term vars -> Core (SObj vars)
seval mode env tm
    = do -- Check the evaluator is initialised. This will fail if the backend
         -- doesn't support scheme evaluation.
         True <- logTimeWhen False "Scheme eval" initialiseSchemeEval
              | False => throw (InternalError "Loading scheme support failed")

         -- make sure all the names in the term are compiled
         -- We need to recheck in advance, since definitions might have changed
         -- since we last evaluated a name, and we might have evaluated the
         -- name in a different mode
         let ms = getRefs (MN "" 0) tm
         let rs = addMetas False ms tm
         names <- getAllNames empty (keys rs)
         traverse_ (compileDef mode) (keys names)

         i <- newRef Sym 0
         (bind, schEnv) <- mkEnv env id
         stm <- compile schEnv !(toFullNames tm)
         Just res <- coreLift $ evalSchemeObj (bind stm)
              | Nothing => throw (InternalError "Compiling expression failed")
         pure (MkSObj res schEnv)
  where
    mkEnv : forall vars . Ref Sym Integer =>
            Env Term vars ->
            (SchemeObj Write -> SchemeObj Write) ->
            Core (SchemeObj Write -> SchemeObj Write, SchVars vars)
    mkEnv [] k = pure (k, [])
    mkEnv (Let fc c val ty :: es) k
        = do i <- nextName
             (bind, vs) <- mkEnv es k
             val' <- compile vs val
             let n = "let-var-" ++ show i
             pure (\x => Let n val' (bind x), Bound n :: vs)
    mkEnv (_ :: es) k
        = do i <- nextName
             (bind, vs) <- mkEnv es k
             pure (bind, Free ("free-" ++ show i) :: vs)

invalid : Core (Term vs)
invalid = pure (Erased emptyFC False)

invalidS : Core (SNF vs)
invalidS = pure (SErased emptyFC False)

getArgList : ForeignObj -> List ForeignObj
getArgList obj
    = if isPair obj
         then unsafeFst obj :: getArgList (unsafeSnd obj)
         else []

quoteFC : ForeignObj -> FC
quoteFC fc_in = fromMaybe emptyFC (fromScheme (decodeObj fc_in))

quoteLazyReason : ForeignObj -> LazyReason
quoteLazyReason r_in = fromMaybe LUnknown (fromScheme (decodeObj r_in))

quoteTypeLevel : ForeignObj -> Name
quoteTypeLevel u_in = fromMaybe (MN "top" 0) (fromScheme (decodeObj u_in))

quoteRigCount : ForeignObj -> RigCount
quoteRigCount rig_in = fromMaybe top (fromScheme (decodeObj rig_in))

quoteBinderName : ForeignObj -> Name
quoteBinderName nm_in
  = fromMaybe (UN (Basic "x")) (fromScheme (decodeObj nm_in))

quoteOrInvalid : Scheme x =>
              ForeignObj -> (x -> Core (Term vars)) -> Core (Term vars)
quoteOrInvalid obj_in k = do
  let Just obj = fromScheme (decodeObj obj_in)
    | Nothing => invalid
  k obj

quoteOrInvalidS : Scheme x =>
                 ForeignObj -> (x -> Core (SNF vars)) -> Core (SNF vars)
quoteOrInvalidS obj_in k = do
  let Just obj = fromScheme (decodeObj obj_in)
    | Nothing => invalidS
  k obj

mutual

  -- We don't use decodeObj because then we have to traverse the term twice.
  -- Instead, decode the ForeignObj directly, which is uglier but faster.
  quoteVector : Ref Sym Integer =>
                Ref Ctxt Defs =>
                SchVars (outer ++ vars) ->
                Integer -> List ForeignObj ->
                Core (Term (outer ++ vars))
  quoteVector svs (-2) [_, fname_in, args_in] -- Blocked app
      = quoteOrInvalid fname_in $ \ fname => do
           let argList = getArgList args_in
           args <- traverse (quote' svs) argList
           pure (apply emptyFC (Ref emptyFC Func fname) args)
  quoteVector svs (-10) [_, fn_arity, args_in] -- Blocked meta app
      = quoteOrInvalid {x = (Name, Integer)} fn_arity $ \ (fname, arity_in) => do
           let arity : Nat = cast arity_in
           let argList = getArgList args_in
           args <- traverse (quote' svs) argList
           defs <- get Ctxt
           fnameF <- toFullNames fname
           (idx, _) <- getPosition fname (gamma defs)
           pure (apply emptyFC (Meta emptyFC fnameF idx (take arity args))
                               (drop arity args))
  quoteVector svs (-11) [_, loc_in, args_in] -- Blocked local var application
      = do loc <- quote' svs loc_in
           let argList = getArgList args_in
           args <- traverse (quote' svs) argList
           pure (apply emptyFC loc args)
  quoteVector svs (-1) (_ :: tag_in :: strtag :: cname_in :: fc_in :: args_in) -- TyCon
      = quoteOrInvalid cname_in $ \ cname =>
        quoteOrInvalid {x = Integer} tag_in $ \ tag => do
           let fc = emptyFC -- quoteFC fc_in
           args <- traverse (quote' svs) args_in
           pure (apply fc (Ref fc (TyCon (cast tag) (length args)) cname)
                           args)
  quoteVector svs (-15) [_, r_in, ty_in] -- Delayed
      = do ty <- quote' svs ty_in
           let r = quoteLazyReason r_in
           pure (TDelayed emptyFC r ty)
  quoteVector svs (-4) [_, r_in, fc_in, ty_in, tm_in] -- Delay
      = do -- Block further reduction under tm_in
           Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #t)"
                | Nothing => invalid
           let Procedure tmproc = decodeObj tm_in
                | _ => invalid
           let Procedure typroc = decodeObj ty_in
                | _ => invalid
           tm <- quote' svs (unsafeForce tmproc)
           ty <- quote' svs (unsafeForce typroc)
           -- Turn blocking off again
           Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #f)"
                | Nothing => invalid
           let fc = quoteFC fc_in
           let r = quoteLazyReason r_in
           pure (TDelay fc r ty tm)
  quoteVector svs (-5) [_, r_in, fc_in, tm_in] -- Force
      = do -- The thing we were trying to force was stuck. Corresponding to
           -- Core.Normalise, reduce it anyway here (so no ct-blockAll like above)
           tm <- quote' svs tm_in
           let fc = quoteFC fc_in
           let r = quoteLazyReason r_in
           pure (TForce fc r tm)
  quoteVector svs (-6) [_, fc_in, imp_in] -- Erased
      = do let fc = quoteFC fc_in
           let imp = case fromScheme (decodeObj imp_in) of
                          Just imp => imp
                          _ => False
           pure (Erased fc imp)
  quoteVector svs (-7) [_, fc_in, u_in] -- Type
      = do let fc = quoteFC fc_in
           let u = quoteTypeLevel u_in
           pure (TType fc u)
  quoteVector svs (-8) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Lambda
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- quote' svs ty_in
           pi <- quotePiInfo svs pi_in
           quoteBinder svs Lam proc_in rig pi ty name
  quoteVector svs (-3) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Pi
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- quote' svs ty_in
           pi <- quotePiInfo svs pi_in
           quoteBinder svs Pi proc_in rig pi ty name
  quoteVector svs (-12) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- PVar
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- quote' svs ty_in
           pi <- quotePiInfo svs pi_in
           quoteBinder svs PVar proc_in rig pi ty name
  quoteVector svs (-13) [_, proc_in, rig_in, ty_in, name_in] -- PVTy
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- quote' svs ty_in
           quoteBinder svs (\fc, r, p, t => PVTy fc r t) proc_in rig Explicit ty name
  quoteVector svs (-14) [_, proc_in, rig_in, val_in, ty_in, name_in] -- PLet
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- quote' svs ty_in
           val <- quote' svs val_in
           quotePLet svs proc_in rig val ty name
  quoteVector svs (-9) [_, blocked, _] -- Blocked top level lambda
      = quote' svs blocked
  quoteVector svs (-100) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I x')
  quoteVector svs (-101) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I8 x')
  quoteVector svs (-102) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I16 x')
  quoteVector svs (-103) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I32 x')
  quoteVector svs (-104) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I64 x')
  quoteVector svs (-105) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (BI x')
  quoteVector svs (-106) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B8 x')
  quoteVector svs (-107) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B16 x')
  quoteVector svs (-108) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B32 x')
  quoteVector svs (-109) [_, x]
      = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B64 x')
  quoteVector svs tag (_ :: cname_in :: fc_in :: args_in) -- DataCon
      = if tag >= 0
           then quoteOrInvalid cname_in $ \ cname =>  do
             let fc = emptyFC -- quoteFC fc_in
             args <- traverse (quote' svs) args_in
             pure (apply fc (Ref fc (DataCon (cast tag) (length args)) cname)
                            args)
           else invalid
  quoteVector _ _ _ = invalid

  quotePiInfo : Ref Sym Integer =>
                Ref Ctxt Defs =>
                SchVars (outer ++ vars) ->
                ForeignObj ->
                Core (PiInfo (Term (outer ++ vars)))
  quotePiInfo svs obj
      = if isInteger obj
           then case unsafeGetInteger obj of
                     0 => pure Implicit
                     1 => pure Explicit
                     2 => pure AutoImplicit
                     _ => pure Explicit
           else if isBox obj
                   then do t' <- quote' svs (unsafeUnbox obj)
                           pure (DefImplicit t')
           else pure Explicit

  quoteBinder : Ref Sym Integer =>
                Ref Ctxt Defs =>
                SchVars (outer ++ vars) ->
                (forall ty . FC -> RigCount -> PiInfo ty -> ty -> Binder ty) ->
                ForeignObj -> -- body of binder, represented as a function
                RigCount ->
                PiInfo (Term (outer ++ vars)) ->
                Term (outer ++ vars) -> -- decoded type
                Name -> -- bound name
                Core (Term (outer ++ vars))
  quoteBinder svs binder proc_in r pi ty name
      = do let Procedure proc = decodeObj proc_in
                    | _ => invalid
           i <- nextName
           let n = show name ++ "-" ++ show i
           let sc = unsafeApply proc (makeSymbol n)
           sc' <- quote' {outer = name :: outer} (Bound n :: svs) sc
           pure (Bind emptyFC name
                      (binder emptyFC r pi ty)
                      sc')

  quotePLet : Ref Sym Integer =>
              Ref Ctxt Defs =>
              SchVars (outer ++ vars) ->
              ForeignObj -> -- body of binder, represented as a function
              RigCount ->
              Term (outer ++ vars) -> -- decoded type
              Term (outer ++ vars) -> -- decoded value
              Name -> -- bound name
              Core (Term (outer ++ vars))
  quotePLet svs proc_in r val ty name
      = do let Procedure proc = decodeObj proc_in
                    | _ => invalid
           i <- nextName
           let n = show name ++ "-" ++ show i
           let sc = unsafeApply proc (makeSymbol n)
           sc' <- quote' {outer = name :: outer} (Bound n :: svs) sc
           pure (Bind emptyFC name
                      (PLet emptyFC r val ty)
                      sc')

  quote' : Ref Sym Integer =>
           Ref Ctxt Defs =>
           SchVars (outer ++ vars) -> ForeignObj ->
           Core (Term (outer ++ vars))
  quote' svs obj
      = if isVector obj
           then quoteVector svs (unsafeGetInteger (unsafeVectorRef obj 0))
                                (unsafeVectorToList obj)
        else if isProcedure obj then quoteBinder svs Lam obj top
                                              Explicit
                                              (Erased emptyFC False)
                                              (UN (Basic "x"))
        else if isSymbol obj then pure $ findName svs (unsafeReadSymbol obj)
        else if isFloat obj then pure $ PrimVal emptyFC (Db (unsafeGetFloat obj))
        else if isInteger obj then pure $ PrimVal emptyFC (I (cast (unsafeGetInteger obj)))
        else if isString obj then pure $ PrimVal emptyFC (Str (unsafeGetString obj))
        else if isChar obj then pure $ PrimVal emptyFC (Ch (unsafeGetChar obj))
        else invalid
    where
      findName : forall vars . SchVars vars -> String -> Term vars
      findName [] n = Ref emptyFC Func (UN (Basic n))
      findName (x :: xs) n
          = if getName x == n
               then Local emptyFC Nothing _ First
               else let Local fc loc _ p = findName xs n
                           | _ => Ref emptyFC Func (UN (Basic n)) in
                        Local fc loc _ (Later p)

      readVector : Integer -> Integer -> ForeignObj -> List ForeignObj
      readVector len i obj
          = if len == i
               then []
               else unsafeVectorRef obj i :: readVector len (i + 1) obj

-- Quote a scheme value directly back to a Term, without making an SNF
-- in between. This is what we want if we're just looking for a normal
-- form immediately (so, evaluating under binders)
export
quoteObj : {auto c : Ref Ctxt Defs} ->
           SObj vars -> Core (Term vars)
quoteObj (MkSObj val schEnv)
    = do i <- newRef Sym 0
         quote' {outer = []} schEnv val

mutual
  snfVector : Ref Ctxt Defs =>
              SchVars vars ->
              Integer -> List ForeignObj ->
              Core (SNF vars)
  snfVector svs (-2) [_, fname_in, args_in] -- Blocked application
      = quoteOrInvalidS fname_in $ \ fname => do
           let args = map (snf' svs) (getArgList args_in)
           pure (SApp emptyFC (SRef Func fname) args)
  snfVector svs (-10) [_, fn_arity, args_in] -- Block meta app
      = quoteOrInvalidS {x = (Name, Integer)} fn_arity $ \ (fname, arity_in) => do
           let arity : Nat = cast arity_in
           let args = map (snf' svs) (getArgList args_in)
           defs <- get Ctxt
           fnameF <- toFullNames fname
           (idx, _) <- getPosition fnameF (gamma defs)
           pure (SApp emptyFC (SMeta fnameF idx (take arity args))
                               (drop arity args))
  snfVector svs (-11) [_, loc_in, args_in] -- Blocked local var application
      = do SApp fc loc args <- snf' svs loc_in
                | _ => invalidS
           let args' = map (snf' svs) (getArgList args_in)
           pure (SApp fc loc (args ++ args'))
  snfVector svs (-1) (_ :: tag_in :: strtag :: cname_in :: fc_in :: args_in) -- TyCon
      = quoteOrInvalidS cname_in $ \ cname =>
        quoteOrInvalidS {x = Integer} tag_in $ \ tag => do
           let fc = quoteFC fc_in
           let args = map (snf' svs) args_in
           pure (STCon fc cname (cast tag) (length args) args)
  snfVector svs (-15) [_, r_in, ty_in] -- Delayed
      = do ty <- snf' svs ty_in
           let r = quoteLazyReason r_in
           pure (SDelayed emptyFC r ty)
  snfVector svs (-4) [_, r_in, fc_in, ty_in, tm_in] -- Delay
      = do let Procedure tmproc = decodeObj tm_in
                | _ => invalidS
           let Procedure typroc = decodeObj ty_in
                | _ => invalidS
           -- Block further reduction under tm_in
           let tm = do Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #t)"
                            | Nothing => invalidS
                       res <- snf' svs (unsafeForce tmproc)
                       Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #f)"
                            | Nothing => invalidS
                       pure res
           let ty = snf' svs (unsafeForce typroc)
           let fc = quoteFC fc_in
           let r = quoteLazyReason r_in
           pure (SDelay fc r ty tm)
  snfVector svs (-5) [_, r_in, fc_in, tm_in] -- Force
      = do -- The thing we were trying to force was stuck. Corresponding to
           -- Core.Normalise, reduce it anyway here (so no ct-blockAll like above)
           tm <- snf' svs tm_in
           let fc = quoteFC fc_in
           let r = quoteLazyReason r_in
           pure (SForce fc r tm)
  snfVector svs (-6) [_, fc_in, imp_in] -- Erased
      = do let fc = quoteFC fc_in
           let imp = case fromScheme (decodeObj imp_in) of
                          Just imp => imp
                          _ => False
           pure (SErased fc imp)
  snfVector svs (-7) [_, fc_in, u_in] -- Type
      = do let fc = quoteFC fc_in
           let u = quoteTypeLevel u_in
           pure (SType fc u)
  snfVector svs (-8) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Lambda
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- snf' svs ty_in
           pi <- snfPiInfo svs pi_in
           snfBinder svs Lam proc_in rig pi ty name
  snfVector svs (-3) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Pi
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- snf' svs ty_in
           pi <- snfPiInfo svs pi_in
           snfBinder svs Pi proc_in rig pi ty name
  snfVector svs (-12) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- PVar
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- snf' svs ty_in
           pi <- snfPiInfo svs pi_in
           snfBinder svs PVar proc_in rig pi ty name
  snfVector svs (-13) [_, proc_in, rig_in, ty_in, name_in] -- PVTy
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- snf' svs ty_in
           snfBinder svs (\fc, r, p, t => PVTy fc r t) proc_in rig Explicit ty name
  snfVector svs (-14) [_, proc_in, rig_in, val_in, ty_in, name_in] -- PLet
      = do let name = quoteBinderName name_in
           let rig = quoteRigCount rig_in
           ty <- snf' svs ty_in
           val <- snf' svs val_in
           snfPLet svs proc_in rig val ty name
  snfVector svs (-9) [_, blocked, _] -- Blocked top level lambda
      = snf' svs blocked

  -- constants here
  snfVector svs (-100) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I x')
  snfVector svs (-101) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I8 x')
  snfVector svs (-102) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I16 x')
  snfVector svs (-103) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I32 x')
  snfVector svs (-104) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I64 x')
  snfVector svs (-105) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (BI x')
  snfVector svs (-106) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B8 x')
  snfVector svs (-107) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B16 x')
  snfVector svs (-108) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B32 x')
  snfVector svs (-109) [_, x]
      = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B64 x')

  snfVector svs tag (_ :: cname_in :: fc_in :: args_in) -- DataCon
      = if tag >= 0
           then quoteOrInvalidS cname_in $ \ cname => do
             let fc = quoteFC fc_in
             let args = map (snf' svs) args_in
             pure (SDCon fc cname (cast tag) (length args) args)
           else invalidS
  snfVector _ _ _ = invalidS

  snfPiInfo : Ref Ctxt Defs =>
              SchVars vars ->
              ForeignObj ->
              Core (PiInfo (SNF vars))
  snfPiInfo svs obj
      = if isInteger obj
           then case unsafeGetInteger obj of
                     0 => pure Implicit
                     1 => pure Explicit
                     2 => pure AutoImplicit
                     _ => pure Explicit
           else if isBox obj
                   then do t' <- snf' svs (unsafeUnbox obj)
                           pure (DefImplicit t')
           else pure Explicit

  snfBinder : Ref Ctxt Defs =>
              SchVars vars ->
              (forall ty . FC -> RigCount -> PiInfo ty -> ty -> Binder ty) ->
              ForeignObj -> -- body of binder, represented as a function
              RigCount ->
              PiInfo (SNF vars) ->
              SNF vars -> -- decoded type
              Name -> -- bound name
              Core (SNF vars)
  snfBinder svs binder proc_in r pi ty name
      = do let Procedure proc = decodeObj proc_in
                    | _ => invalidS
           pure (SBind emptyFC name (binder emptyFC r pi ty)
                       (\tm => do let MkSObj arg _ = tm
                                  let sc = unsafeApply proc arg
                                  snf' svs sc))

  snfPLet : Ref Ctxt Defs =>
            SchVars vars ->
            ForeignObj -> -- body of binder, represented as a function
            RigCount ->
            SNF vars -> -- decoded type
            SNF vars -> -- decoded value
            Name -> -- bound name
            Core (SNF vars)
  snfPLet svs proc_in r val ty name
      = do let Procedure proc = decodeObj proc_in
                    | _ => invalidS
           pure (SBind emptyFC name (PLet emptyFC r val ty)
                       (\tm => do let MkSObj arg _ = tm
                                  let sc = unsafeApply proc arg
                                  snf' svs sc))

  snf' : Ref Ctxt Defs =>
         SchVars vars -> ForeignObj ->
         Core (SNF vars)
  snf' svs obj
      = if isVector obj
           then snfVector svs (unsafeGetInteger (unsafeVectorRef obj 0))
                              (unsafeVectorToList obj)
           else if isProcedure obj then snfBinder svs Lam obj top
                                                 Explicit
                                                 (SErased emptyFC False)
                                                 (UN (Basic "x"))
           else if isSymbol obj then pure $ findName svs (unsafeReadSymbol obj)
           else if isFloat obj then pure $ SPrimVal emptyFC (Db (unsafeGetFloat obj))
           else if isInteger obj then pure $ SPrimVal emptyFC (I (cast (unsafeGetInteger obj)))
           else if isString obj then pure $ SPrimVal emptyFC (Str (unsafeGetString obj))
           else if isChar obj then pure $ SPrimVal emptyFC (Ch (unsafeGetChar obj))
           else invalidS
    where
      findName : forall vars . SchVars vars -> String -> SNF vars
      findName [] n = SApp emptyFC (SRef Func (UN (Basic n))) []
      findName (x :: xs) n
          = if getName x == n
               then SApp emptyFC (SLocal _ First) []
               else let SApp fc (SLocal _ p) args = findName xs n
                           | _ => SApp emptyFC (SRef Func (UN (Basic n))) [] in
                        SApp fc (SLocal _ (Later p)) []

      readVector : Integer -> Integer -> ForeignObj -> List ForeignObj
      readVector len i obj
          = if len == i
               then []
               else unsafeVectorRef obj i :: readVector len (i + 1) obj

export
toSNF : Ref Ctxt Defs =>
        SObj vars -> Core (SNF vars)
toSNF (MkSObj val schEnv) = snf' schEnv val


text:
module Main

greet : Eff () [STDIO]
greet = do putStrLn "Hello world"
		putStrLn "What is your name?"
        x <- getStr
        putStrLn ("Welcome, " ++ trim x)

main : IO ()
main = run greet

--Run:
--$ idris greet.idr -o greet
--$ ./greet

max_stars_repo_name: coyote-dev/Hello-World

max_issues_repo_name: coyote-dev/Hello-World

max_forks_repo_name: coyote-dev/Hello-World


text:
module Control.Algebra.ZZBezoutsIdentity

import Control.Algebra
import Classes.Verified

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.AlgebraicVerified 	-- for (ringNeutralIsMultZeroL)

import Control.Algebra.ZZDivisors

import Data.Fin.FinOrdering
import Data.Fin.Structural

import Control.Isomorphism

-- Dependent pattern matching using (do) notation binds improves clarity
import Control.Monad.Identity
import Syntax.PreorderReasoning

import Control.Algebra.DiamondInstances

-- For example
import Data.ZZ.ZZModulo

{-
Table of contents:
* Lemmas for verifying the euclidean algorithm (bezoutsIdentityZZIfModulo)
* (bezoutsIdentityZZIfModulo) implementation
* (Commentary) "Goal: Separation of algorithm from verification."
* The GCD derived from (modZT), itself derived from (modNatT).
-}

{-
Lemmas for verifying the euclidean algorithm (bezoutsIdentityZZIfModulo)
-}

total
bezoutsIdentityLincombEqZZ :
	(a, b, c, d, q, r : ZZ)
	-> q<.>d = c <-> r
	-> b<.>c <+> (a <-> b <.> q)<.>d
		= a<.>d <+> b<.>r
bezoutsIdentityLincombEqZZ a b c d q r pr =
	(
	b<.>c <+> (a <-> b <.> q)<.>d
	) ={
		cong {f=((b<.>c) <+>)}
		$ (
		(a <-> b <.> q)<.>d
		) ={ ringOpIsDistributiveSubR _ _ _ }= (
		a<.>d <-> (b<.>q)<.>d
		) ={
			cong {f=((a<.>d) <->)}
			{- Bracketing style switch -}
			$ ( b<.>q<.>d ) ={ sym $ ringOpIsAssociative b q d }=
			( b<.>(q<.>d) ) ={ cong {f=(b<.>)} pr }=
			( b<.>(c <-> r) ) QED
			}= (
		a<.>d <-> b<.>(c <-> r)
		) ={ abelianGroupOpIsCommutative (a <.> d) _ }= (
		(inverse $ b<.>(c <-> r)) <+> a <.> d
		) QED
		}= (
	b <.> c <+> ( (inverse $ b<.>(c <-> r)) <+> a <.> d )
	) ={ semigroupOpIsAssociative _ _ _ }= (
	b <.> c <-> b<.>(c <-> r) <+> a <.> d
	) ={ abelianGroupOpIsCommutative _ (a <.> d) }= (
	a <.> d <+> ( b <.> c <-> b<.>(c <-> r) )
	) ={
		cong {f=((a <.> d) <+>)}
		$ trans (sym $ ringOpIsDistributiveSubL _ _ _)
		$ cong {f=(b<.>)}
		{- Bracketing style switch -}
		$ ( c <-> (c <-> r) )
			={
				cong {f=(c<+>)}
				$ trans (ringOpIsDistributiveR _ _ _)
				$ cong {f=((inverse c) <+>)}
				$ inverseIsInvolution r
				}=
		( c <+> (inverse c <+> r) )
			={ semigroupOpIsAssociative c (inverse c) r }=
		( (c <-> c) <+> r )
			={ cong {f=(<+> r)} $ groupInverseIsInverseL c }=
		( Algebra.neutral <+> r )
			={ monoidNeutralIsNeutralR _ }=
		( r ) QED
		}= (
	a<.>d <+> b<.>r
	) QED

total
bezoutsIdentityExtQuotientLincombZZ :
	(c, d, q, r, x : ZZ)
	-> (q<.>d <+> r = c)
	-> (d `quotientOverZZ` x)
	-> (r `quotientOverZZ` x)
	-> (c `quotientOverZZ` x)
bezoutsIdentityExtQuotientLincombZZ c d q r x eqpr (dq ** dqPr) (rq ** rqPr)
	= (q<.>dq <+> rq
	** trans (ringOpIsDistributiveR (q<.>dq) rq x)
	$ rewrite rqPr
	in trans ( cong { f= (<+>r) }
		$ trans (sym $ ringOpIsAssociative _ _ _)
		$ cong {f=(q<.>)} $ dqPr )
	$ eqpr)

total
bezQTy : (c, d, a, b : ZZ) -> Type
bezQTy c d a b =
	( c `quotientOverZZ` (a<.>c <+> b<.>d)
	, d `quotientOverZZ` (a<.>c <+> b<.>d) )

{-
(bezoutsIdentityZZIfModulo) implementation

Given a modulo operator giving the remainder in a remainder-division pair,
produce a linear combination of two input integers which divides them both.

Since every number dividing both integers divides every linear combination
of them, this gives the greatest common denominator.

The latter statement isn't proved here, though.
-}

{- (bezoutsIdentityZZIfModulo) parameters -}
parameters (
	{-
	The nonnegative residue of the 1st modulo the subgroup generated by the 2nd.
	Can factor through a modulo on naturals, but must be everywhere defined.
	-}
	modZ : ZZ -> ZZ -> ZZ
	, quotientPartZ : (x, m : ZZ) -> (x <-> modZ x m) `quotientOverZZ` m
	) {

bezoutsIdentityZZIfModulo :
	( c, d : ZZ )
	-> ( zpar : (ZZ, ZZ) ** uncurry (bezQTy c d) zpar )
-- bezoutsIdentityZZIfModulo c (Pos Z) = ( (1, 0) ** ((1 ** _), (0 ** _)) )
bezoutsIdentityZZIfModulo c (Pos Z) = ( (Algebra.unity, Algebra.neutral)
	** rewrite ringWithUnityIsUnityR c
		in rewrite monoidNeutralIsNeutralL c
		in ( (Algebra.unity ** ringWithUnityIsUnityR c)
			, (Algebra.neutral ** ringNeutralIsMultZeroL c) ) )
bezoutsIdentityZZIfModulo c d with (bezoutsIdentityZZIfModulo d (c `modZ` d))
	| ((a,b) ** oldpr) = runIdentity $ do {
			(q ** qIsDivD) <- Id $ c `quotientPartZ` d
			((a' ** divsPrA), (b' ** divsPrB)) <- Id $ oldpr
			-- reverifyDivZ across the bind
			let reverifyDivZ' =
				trans (cong {f=(<+> (c `modZ` d))} qIsDivD)
				$ groupSubtractionIsRDivision c $ c `modZ` d
			-- the goal linear combo of c & d gives d `gcd` (c `modZ` d)
			let lincombEq = bezoutsIdentityLincombEqZZ
				a b c d q (c `modZ` d)
				$ groupDivisionAddLToSubR
					(q <.> d) (c `modZ` d) c
					$ reverifyDivZ'
			-- d `gcd` (c `modZ` d) | c
			let extQuotientLincombZZ = bezoutsIdentityExtQuotientLincombZZ
				c d q (c `modZ` d) ( a<.>d <+> b<.>(c `modZ` d) )
				reverifyDivZ'
				(a' ** divsPrA)
				(b' ** divsPrB)
			return $ ( (b, a <-> b <.> q)
				** ((getWitness extQuotientLincombZZ
					** trans (cong lincombEq)
					$ getProof extQuotientLincombZZ)
				, (a' ** trans (cong lincombEq) divsPrA)) )
		}

} {- (bezoutsIdentityZZIfModulo) parameters -}

{-
Goal: Separation of algorithm from verification.
Obstructions: (Problem 1), (Problem 2).

divZ : ZZ -> ZZ -> ZZ
divZ a b = getWitness $ quotientPartZ a b

reverifyDivZ : divZ a b <.> b <+> modZ a b = a
reverifyDivZ {a} {b}
	= trans (cong {f=(<+> (a `modZ` b))}
		$ getProof $ quotientPartZ a b)
	$ groupSubtractionIsRDivision a $ a `modZ` b

||| Greatest Common Denominator (GCD) linear combination factors
euclideanAlgPar : ZZ -> ZZ -> (ZZ, ZZ)
euclideanAlgPar c (Pos Z) = (1, 0)
euclideanAlgPar c d = (b, a <-> b <.> q)
	where
		eucParReduced : (ZZ, ZZ)
		eucParReduced = euclideanAlgPar d (c `modZ` d)
		a : ZZ
		a = fst eucParReduced
		b : ZZ
		b = snd eucParReduced
		q : ZZ
		q = c `divZ` d

||| Greatest Common Denominator (GCD)
euclideanAlg : ZZ -> ZZ -> ZZ
euclideanAlg c d = let (a, b) = euclideanAlgPar c d in a<.>c <+> b<.>d

bezoutsIdentity : (c, d : ZZ) -> uncurry (bezQTy c d) $ euclideanAlgPar c d

---
Problem 1)
rewrite did not change type uncurry (bezQTy c (Pos 0)) (euclideanAlgPar c (Pos 0))
---

bezoutsIdentity c (Pos Z)
	= rewrite ringWithUnityIsUnityR c
	in rewrite monoidNeutralIsNeutralL c
	in ( (Algebra.unity ** ringWithUnityIsUnityR c)
		, (Algebra.neutral ** ringNeutralIsMultZeroL c) )

---
Problem 2)
Proof must be repeated for positive and negative halves,
since otherwise the case can't be determined to not be the one for 2nd argument 0.
---

bezoutsIdentity c d@(Pos $ S d') = ?bezoutsIdentity_rhs_2
bezoutsIdentity c d@(NegS d') = ?bezoutsIdentity_rhs_3

-}

{-
The GCD derived from (modZT), itself derived from (modNatT).
-}

bezoutZT :
	( c, d : ZZ )
	-> ( zpar : (ZZ, ZZ) ** uncurry (bezQTy c d) zpar )
bezoutZT = bezoutsIdentityZZIfModulo modZT quotientPartModZT


text:
module System.Path

import Data.List
import Data.List1
import Data.Maybe
import Data.Nat
import Data.String
import Data.String.Extra

import Text.Token
import Text.Lexer
import Text.Parser
import Text.Quantity

import System.Info

infixr 5 </>, />
infixr 7 <.>

||| The character that separates directories in the path.
export
dirSeparator : Char
dirSeparator = if isWindows then '\\' else '/'

||| The character that separates multiple paths.
export
pathSeparator : Char
pathSeparator = if isWindows then ';' else ':'

||| Windows path prefix.
public export
data Volume
  =
  ||| Windows Uniform Naming Convention, consisting of server name and share
  ||| directory.
  |||
  ||| Example: `\\localhost\share`
  UNC String String |
  ||| The drive.
  |||
  ||| Example: `C:`
  Disk Char

||| A single body in path.
public export
data Body
  =
  ||| Represents ".".
  CurDir |
  ||| Represents "..".
  ParentDir |
  ||| Directory or file.
  Normal String

||| A parsed cross-platform file system path.
|||
||| Use the function `parse` to constructs a Path from String, and use the
||| function `show` to convert in reverse.
|||
||| Trailing separator is only used for display and is ignored when comparing
||| paths.
public export
record Path where
    constructor MkPath
    ||| Windows path prefix (only for Windows).
    volume : Maybe Volume
    ||| Whether the path contains root.
    hasRoot : Bool
    ||| Path bodies.
    body : List Body
    ||| Whether the path terminates with a separator.
    hasTrailSep : Bool

export
Eq Volume where
  (==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
  (==) (Disk l) (Disk r) = l == r
  (==) _ _ = False

export
Eq Body where
  (==) CurDir CurDir = True
  (==) ParentDir ParentDir = True
  (==) (Normal l) (Normal r) = l == r
  (==) _ _ = False

export
Eq Path where
  (==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) =
    l1 == r1 && l2 == r2 && l3 == r3

||| An empty path, which represents "".
public export
emptyPath : Path
emptyPath = MkPath Nothing False [] False

--------------------------------------------------------------------------------
-- Show
--------------------------------------------------------------------------------

export
Show Body where
  show CurDir = "."
  show ParentDir = ".."
  show (Normal normal) = normal

export
Show Volume where
  show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
  show (Disk disk) = String.singleton disk ++ ":"

||| Displays the path in the format of this platform.
export
Show Path where
  show path =
    let
      sep = String.singleton dirSeparator
      showVol = maybe "" show path.volume
      showRoot = if path.hasRoot then sep else ""
      showBody = join sep $ map show path.body
      showTrail = if path.hasTrailSep then sep else ""
    in
      showVol ++ showRoot ++ showBody ++ showTrail

--------------------------------------------------------------------------------
-- Parser
--------------------------------------------------------------------------------

data PathTokenKind = PTText | PTPunct Char

Eq PathTokenKind where
  (==) PTText PTText = True
  (==) (PTPunct c1) (PTPunct c2) = c1 == c2
  (==) _ _ = False

PathToken : Type
PathToken = Token PathTokenKind

TokenKind PathTokenKind where
  TokType PTText = String
  TokType (PTPunct _) = ()

  tokValue PTText x = x
  tokValue (PTPunct _) _ = ()

pathTokenMap : TokenMap PathToken
pathTokenMap = toTokenMap $
  [ (is '/', PTPunct '/')
  , (is '\\', PTPunct '\\')
  , (is ':', PTPunct ':')
  , (is '?', PTPunct '?')
  , (some $ non $ oneOf "/\\:?", PTText)
  ]

lexPath : String -> List (WithBounds PathToken)
lexPath str =
  let
    (tokens, _, _, _) = lex pathTokenMap str
  in
    tokens -- TokenData.tok tokens

-- match both '/' and '\\' regardless of the platform.
bodySeparator : Grammar state PathToken True ()
bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')

-- Windows will automatically translate '/' to '\\'. And the verbatim prefix,
-- i.e., `\\?\`, can be used to disable the translation.
-- However, we just parse it and ignore it.
--
-- Example: \\?\
verbatim : Grammar state PathToken True ()
verbatim =
  do
    ignore $ count (exactly 2) $ match $ PTPunct '\\'
    match $ PTPunct '?'
    match $ PTPunct '\\'
    pure ()

-- Example: \\server\share
unc : Grammar state PathToken True Volume
unc =
  do
    ignore $ count (exactly 2) $ match $ PTPunct '\\'
    server <- match PTText
    bodySeparator
    share <- match PTText
    pure $ UNC server share

-- Example: \\?\server\share
verbatimUnc : Grammar state PathToken True Volume
verbatimUnc =
  do
    verbatim
    server <- match PTText
    bodySeparator
    share <- match PTText
    pure $ UNC server share

-- Example: C:
disk : Grammar state PathToken True Volume
disk =
  do
    text <- match PTText
    disk <- case unpack text of
              (disk :: xs) => pure disk
              [] => fail "Expects disk"
    match $ PTPunct ':'
    pure $ Disk (toUpper disk)

-- Example: \\?\C:
verbatimDisk : Grammar state PathToken True Volume
verbatimDisk =
  do
    verbatim
    disk <- disk
    pure disk

parseVolume : Grammar state PathToken True Volume
parseVolume =
      verbatimUnc
  <|> verbatimDisk
  <|> unc
  <|> disk

parseBody : Grammar state PathToken True Body
parseBody =
  do
    text <- match PTText
    pure $ case text of
      ".." => ParentDir
      "." => CurDir
      normal => Normal normal

parsePath : Grammar state PathToken False Path
parsePath =
  do
    vol <- optional parseVolume
    root <- optional (some bodySeparator)
    body <- sepBy (some bodySeparator) parseBody
    trailSep <- optional (some bodySeparator)
    let body = filter (\case Normal s => ltrim s /= ""; _ => True) body
    let body = case body of
                [] => []
                (x::xs) => x :: delete CurDir xs
    pure $ MkPath vol (isJust root) body (isJust trailSep)

||| Parses a String into Path.
|||
||| The string is parsed as much as possible from left to right, and the invalid
||| parts on the right is ignored.
|||
||| Some kind of invalid paths are accepted. The relax rules:
|||
||| - Both slash('/') and backslash('\\') are parsed as valid directory separator,
|||   regardless of the platform;
||| - Any characters in the body in allowed, e.g., glob like "/root/*";
||| - Verbatim prefix(`\\?\`) that disables the forward slash is ignored (for
|||   Windows only).
||| - Repeated separators are ignored, therefore, "a/b" and "a//b" both have "a"
|||   and "b" as bodies.
||| - "." in the body are removed, unless they are at the beginning of the path.
|||   For example, "a/./b", "a/b/", "a/b/." and "a/b" will have "a" and "b" as
|||   bodies, and "./a/b" will starts with `CurDir`.
|||
||| ```idris example
||| parse "C:\\Windows/System32"
||| parse "/usr/local/etc/*"
||| ```
export
parse : String -> Path
parse str =
  case parse parsePath (lexPath str) of
    Right (path, _) => path
    _ => emptyPath

--------------------------------------------------------------------------------
-- Utils
--------------------------------------------------------------------------------

isAbsolute' : Path -> Bool
isAbsolute' path =
  if isWindows then
    case path.volume of
      Just (UNC _ _) => True
      Just (Disk _) => path.hasRoot
      Nothing => False
  else
    path.hasRoot

append' : (left : Path) -> (right : Path) -> Path
append' left right =
  if isAbsolute' right || isJust right.volume then
    right
  else if hasRoot right then
    record { volume = left.volume } right
  else
    record { body = left.body ++ right.body, hasTrailSep = right.hasTrailSep } left

splitPath' : Path -> List Path
splitPath' path =
  case splitRoot path of
    (Just root, other) => root :: iterateBody (path.body) (path.hasTrailSep)
    (Nothing, other) => iterateBody (path.body) (path.hasTrailSep)
  where
    splitRoot : Path -> (Maybe Path, Path)
    splitRoot path@(MkPath Nothing False _ _) = (Nothing, path)
    splitRoot (MkPath vol root xs trailSep) =
      (Just $ MkPath vol root [] False, MkPath Nothing False xs trailSep)

    iterateBody : List Body -> (trailSep : Bool) -> List Path
    iterateBody [] _ = []
    iterateBody [x] trailSep = [MkPath Nothing False [x] trailSep]
    iterateBody (x::y::xs) trailSep =
      (MkPath Nothing False [x] False) :: iterateBody (y::xs) trailSep

splitParent' : Path -> Maybe (Path, Path)
splitParent' path =
  case path.body of
    [] => Nothing
    (x::xs) =>
      let
        parent = record { body = init (x::xs), hasTrailSep = False } path
        child = MkPath Nothing False [last (x::xs)] path.hasTrailSep
      in
        Just (parent, child)

parent' : Path -> Maybe Path
parent' = map fst . splitParent'

fileName' : Path -> Maybe String
fileName' path =
  findNormal $ reverse path.body
where
  findNormal : List Body -> Maybe String
  findNormal ((Normal normal)::xs) = Just normal
  findNormal (CurDir::xs) = findNormal xs
  findNormal _ = Nothing

setFileName' : (name : String) -> Path -> Path
setFileName' name path =
  if isJust (fileName' path) then
    append' (fromMaybe emptyPath $ parent' path) (parse name)
  else
    append' path (parse name)

export
splitFileName : String -> (String, String)
splitFileName name =
  case break (== '.') $ reverse $ unpack name of
    (_, []) => (name, "")
    (_, ['.']) => (name, "")
    (revExt, (dot :: revStem)) =>
      ((pack $ reverse revStem), (pack $ reverse revExt))

--------------------------------------------------------------------------------
-- Methods
--------------------------------------------------------------------------------

||| Returns true if the path is absolute.
|||
||| - On Unix, a path is absolute if it starts with the root, so `isAbsolute` and
|||   `hasRoot` are equivalent.
|||
||| - On Windows, a path is absolute if it starts with a disk and has root or
|||   starts with UNC. For example, `c:\\windows` is absolute, while `c:temp`
|||   and `\temp` are not.
export
isAbsolute : String -> Bool
isAbsolute = isAbsolute' . parse

||| Returns true if the path is relative.
export
isRelative : String -> Bool
isRelative = not . isAbsolute

||| Appends the right path to the left path.
|||
||| If the path on the right is absolute, it replaces the left path.
|||
||| On Windows:
|||
||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
|||   everything except for the volume (if any) of left.
||| - If the right path has a volume but no root, it replaces left.
|||
||| ```idris example
||| parse "/usr" /> "local/etc" == "/usr/local/etc"
||| ```
export
(/>) : (left : Path) -> (right : String) -> Path
(/>) left right = append' left (parse right)

||| Appends the right path to the left path.
|||
||| If the path on the right is absolute, it replaces the left path.
|||
||| On Windows:
|||
||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
|||   everything except for the volume (if any) of left.
||| - If the right path has a volume but no root, it replaces left.
|||
||| ```idris example
||| "/usr" </> "local/etc" == "/usr/local/etc"
||| ```
export
(</>) : (left : String) -> (right : String) -> String
(</>) left right = show $ parse left /> right

||| Joins path components into one.
|||
||| ```idris example
||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
||| ```
export
joinPath : List String -> String
joinPath xs = show $ foldl (/>) (parse "") xs

||| Splits path into components.
|||
||| ```idris example
||| splitPath "/usr/local/etc" == ["/", "usr", "local", "etc"]
||| splitPath "tmp/Foo.idr" == ["tmp", "Foo.idr"]
||| ```
export
splitPath : String -> List String
splitPath = map show . splitPath' . parse

||| Splits the path into parent and child.
|||
||| ```idris example
||| splitParent "/usr/local/etc" == Just ("/usr/local", "etc")
||| ```
export
splitParent : String -> Maybe (String, String)
splitParent path =
  do
    (parent, child) <- splitParent' (parse path)
    pure (show parent, show child)

||| Returns the path without its final component, if there is one.
|||
||| Returns Nothing if the path terminates by a root or volume.
export
parent : String -> Maybe String
parent = map show . parent' . parse

||| Returns the list of all parents of the path, longest first, self included.
|||
||| ```idris example
||| parents "/etc/kernel" == ["/etc/kernel", "/etc", "/"]
||| ```
export
parents : String -> List String
parents = map show . List.iterate parent' . parse

||| Determines whether the base is one of the parents of target.
|||
||| Trailing separator is ignored.
|||
||| ```idris example
||| "/etc" `isBaseOf` "/etc/kernel"
||| ```
export
isBaseOf : (base : String) -> (target : String) -> Bool
isBaseOf base target =
  let
    MkPath baseVol baseRoot baseBody _ = parse base
    MkPath targetVol targetRoot targetBody _ = parse target
  in
       baseVol == targetVol
    && baseRoot == targetRoot
    && (baseBody `isPrefixOf` targetBody)

||| Returns a path that, when appended to base, yields target.
|||
||| Returns Nothing if the base is not a prefix of the target.
export
dropBase : (base : String) -> (target : String) -> Maybe String
dropBase base target =
  do
    let MkPath baseVol baseRoot baseBody _ = parse base
    let MkPath targetVol targetRoot targetBody targetTrialSep = parse target
    if baseVol == targetVol && baseRoot == targetRoot then Just () else Nothing
    body <- dropBody baseBody targetBody
    pure $ show $ MkPath Nothing False body targetTrialSep
  where
    dropBody : (base : List Body) -> (target : List Body) -> Maybe (List Body)
    dropBody [] ys = Just ys
    dropBody xs [] = Nothing
    dropBody (x::xs) (y::ys) = if x == y then dropBody xs ys else Nothing

||| Returns the last body of the path.
|||
||| If the last body is a file, this is the file name;
||| if it's a directory, this is the directory name;
||| if it's ".", it recurses on the previous body;
||| if it's "..", returns Nothing.
export
fileName : String -> Maybe String
fileName  = fileName' . parse

||| Extracts the file name in the path without extension.
|||
||| The stem is:
|||
||| - Nothing, if there is no file name;
||| - The entire file name if there is no embedded ".";
||| - The entire file name if the file name begins with a "." and has no other ".";
||| - Otherwise, the portion of the file name before the last ".".
export
fileStem : String -> Maybe String
fileStem path = pure $ fst $ splitFileName !(fileName path)

||| Extracts the extension of the file name in the path.
|||
||| The extension is:
|||
||| - Nothing, if there is no file name;
||| - Nothing, if there is no embedded ".";
||| - Nothing, if the file name begins with a "." and has no other ".";
||| - Otherwise, the portion of the file name after the last ".".
export
extension : String -> Maybe String
extension path = fileName path >>=
  filter (/= "") . Just . snd . splitFileName

||| Updates the file name in the path.
|||
||| If there is no file name, it appends the name to the path;
||| otherwise, it appends the name to the parent of the path.
export
setFileName : (name : String) -> String -> String
setFileName name path = show $ setFileName' name (parse path)

||| Appends a extension to the path.
|||
||| If there is no file name, the path will not change;
||| if the path has no extension, the extension will be appended;
||| if the given extension is empty, the extension of the path will be dropped;
||| otherwise, the extension will be replaced.
|||
||| ```idris example
||| "/tmp/Foo" <.> "idr" == "/tmp/Foo.idr"
||| ```
export
(<.>) : String -> (extension : String) -> String
(<.>) path ext =
  let
    path' = parse path
    ext = pack $ dropWhile (\char => char == '.' || isSpace char) (unpack ext)
    ext = if ext == "" then "" else "." ++ ext
  in
    case fileName' path' of
      Just name =>
        let (stem, _) = splitFileName name in
          show $ setFileName' (stem ++ ext) path'
      Nothing => path

||| Drops the extension of the path.
export
dropExtension : String -> String
dropExtension path = path <.> ""


text:
-- USAGE: $ idris2 -q -x main shell-effects.idr

-- SRC: https://stackoverflow.com/questions/39812465/how-can-i-call-a-subprocess-in-idris

import System

-- read the contents of a file
readFileH : (fileHandle : File) -> IO String
readFileH h = loop ""
  where
    loop acc = do
      if !(fEOF h) then pure acc
        else do
          Right l <- fGetLine h | Left err => pure acc
          loop (acc ++ l)

execAndReadOutput : (cmd : String) -> IO String
execAndReadOutput cmd = do
  Right fh <- popen cmd Read | Left err => pure ""
  contents <- readFileH fh
  pclose fh
  pure contents

main : IO ()
main = do
  out <- (execAndReadOutput "echo \"Captured output\"")
  putStrLn "Here is what we got:"
  putStr out

max_stars_repo_name: amerlyq/aeternum-langs

max_issues_repo_name: amerlyq/aeternum-langs

max_forks_repo_name: amerlyq/aeternum-langs