text:
module Main
import System.File

import Data.List
import Data.Strings as S
import Data.String.Extra as S
import Data.Maybe

import Idris.Parser

import Parser.Source as PS

import System.File
import System

import Language.APIDef as APIDef

import Idris.Syntax as IS
import Core.TT as CT
import Core.Name as CN
import Core.Name.Namespace as NS

import Text.PrettyPrint.Prettyprinter as PP
import Text.PrettyPrint.Prettyprinter.Doc as PP
import Text.PrettyPrint.Prettyprinter.Util

import Text.PrettyPrint.Prettyprinter.Render.String
showConst : Constant -> String
showConst (I x) = "I "
showConst (BI x) = "BI "
showConst (B8 x) = "BB "
showConst (B16 x) = "B26 "
showConst (B32 x) = "B32 "
showConst (B64 x) = "B64 "
showConst (Str x) = "Str "
showConst (Ch x) = "Ch "
showConst (Db x) = "Db "
showConst WorldVal = "WVal "
showConst IntType = "IntT "
showConst IntegerType = "IntegerT "
showConst Bits8Type = "B8T "
showConst Bits16Type = "B16T "
showConst Bits32Type = "B32T "
showConst Bits64Type = "B64T "
showConst StringType = "StringT "
showConst CharType = "CharT "
showConst DoubleType = "DoubleT "
showConst WorldType = "WorldT "

quote : String -> String
quote x = "(" ++ x ++ ")"

len : List a -> Int
len [] = 0
len (x::xs) = 1 + len xs

constantToConst: Constant -> Const
constantToConst (I x) =     (CI x)
constantToConst (BI x) =    (CBI x)
constantToConst (B8 x) =    (CB8 x)
constantToConst (B16 x) =   (CB16 x)
constantToConst (B32 x) =   (CB32 x)
constantToConst (B64 x) =   (CB64 x)
constantToConst (Str x) =   (CStr x)
constantToConst (Ch x) =    (CCh x)
constantToConst (Db x) =    (CDb x)
constantToConst WorldVal =  CWorldVal
constantToConst IntType =   CIntType
constantToConst IntegerType = CIntegerType
constantToConst Bits8Type = CBits8Type
constantToConst Bits16Type = CBits16Type
constantToConst Bits32Type = CBits32Type
constantToConst Bits64Type = CBits64Type
constantToConst StringType = CStringType
constantToConst CharType = CCharType
constantToConst DoubleType = CDoubleType
constantToConst WorldType = CWorldType

mutual

  convertName : CN.Name -> APIDef.Name
  convertName = show
  -- conversion rule.  PTerm -> DTerm
  export
  convertTerm : IS.PTerm -> DTerm
  convertTerm (PRef fc x) = DRef (convertName x)
  convertTerm (PPi fc x y z argTy retTy) = DPi (convertName <$> z) (convertTerm argTy) (convertTerm retTy)
  convertTerm (PLam fc x y z argTy scope) = DLam (convertTerm z) (convertTerm argTy) (convertTerm scope)
  convertTerm p@(PLet fc x pat nTy nVal scope alts) = DTermNotImplemented (show p)
  convertTerm p@(PCase fc x xs) = DTermNotImplemented ("PCase")
  convertTerm p@(PLocal fc xs scope) = DTermNotImplemented ("PLocal")
  convertTerm p@(PUpdate fc xs) = DTermNotImplemented ("PUpdate")
  convertTerm p@(PApp fc x y) = DApp (convertTerm x) (convertTerm y)
  convertTerm p@(PWithApp fc x y) = DTermNotImplemented ("PWithApp")
  convertTerm p@(PNamedApp fc x y z) = DNamedApp (convertTerm x) (convertName y) (convertTerm z)
  convertTerm p@(PAutoApp fc x y) = DTermNotImplemented ("PAutoApp")
  convertTerm p@(PDelayed fc x y) = DTermNotImplemented ("PDelayed")
  convertTerm p@(PDelay fc x) = DTermNotImplemented ("PDelay")
  convertTerm p@(PForce fc x) = DTermNotImplemented ("PForce")
  convertTerm p@(PSearch fc depth) = DTermNotImplemented ("PSearch")
  convertTerm p@(PPrimVal fc x) = DPrimVal (constantToConst x)
  convertTerm p@(PQuote fc x) = DTermNotImplemented ("PQuote")
  convertTerm p@(PQuoteName fc x) = DTermNotImplemented ("PQuoteName")
  convertTerm p@(PQuoteDecl fc xs) = DTermNotImplemented ("PQuoteDecl")
  convertTerm p@(PUnquote fc x) = DTermNotImplemented ("PUnquote")
  convertTerm p@(PRunElab fc x) = DTermNotImplemented ("PRunElab")
  convertTerm p@(PHole fc bracket holename) = DHole (show holename)
  convertTerm p@(PType fc) = DType
  convertTerm p@(PAs fc nfc x pattern) = DTermNotImplemented ("PAs")
  convertTerm p@(PDotted fc x) = DTermNotImplemented ("PDotted")
  convertTerm p@(PImplicit fc) = DImplicit
  convertTerm p@(PInfer fc) = DInfer
  convertTerm p@(POp fc x y z) = DTermNotImplemented ("POp")
  convertTerm p@(PPrefixOp fc x y) = DTermNotImplemented ("PPrefixOp")
  convertTerm p@(PSectionL fc x y) = DTermNotImplemented ("PSectionL")
  convertTerm p@(PSectionR fc x y) = DTermNotImplemented ("PSectionR")
  convertTerm p@(PEq fc x y) = DTermNotImplemented ("PEq")
  convertTerm p@(PBracketed fc x) = DBracketed (convertTerm x)

  convertTerm p@(PString fc ls) = DTermNotImplemented ("PString")
  convertTerm p@(PMultiline fc i lls) = DTermNotImplemented ("PMultiline")
  convertTerm p@(PDoBlock fc x xs) = DTermNotImplemented ("PDoBlock")
  convertTerm p@(PBang fc x) = DTermNotImplemented ("PBang")
  convertTerm p@(PIdiom fc x) = DTermNotImplemented ("PIdiom")
  convertTerm p@(PList fc xs) = DList (map convertTerm xs)
  convertTerm p@(PPair fc x y) = DPair (convertTerm x) (convertTerm y)
  convertTerm p@(PDPair fc x y z) = DTermNotImplemented ("PDPair")
  convertTerm p@(PUnit fc) = DUnit
  convertTerm p@(PIfThenElse fc x y z) = DTermNotImplemented ("PIfThenElse")
  convertTerm p@(PComprehension fc x xs) = DTermNotImplemented ("PComprehension")
  convertTerm p@(PRewrite fc x y) = DTermNotImplemented ("PRewrite")
  convertTerm p@(PRange fc x y z) = DTermNotImplemented ("PRange")
  convertTerm p@(PRangeStream fc x y) = DTermNotImplemented ("PRangeStream")
  convertTerm p@(PPostfixApp fc x xs) = DTermNotImplemented ("PPostfixApp")
  convertTerm p@(PPostfixAppPartial fc xs) = DTermNotImplemented ("PPostfixAppPartial")
  convertTerm p@(PUnifyLog fc x y) = DTermNotImplemented ("PUnifyLog")
  convertTerm p@(PWithUnambigNames fc xs x) = DTermNotImplemented ("PWithUnambigNames")

  convertClause : IS.PClause -> DClause
  convertClause (MkPatClause fc lhs rhs whereblock) = MkDPatClause (convertTerm lhs) (convertTerm rhs)
  convertClause (MkWithClause fc lhs wval xs ys zs) = MkDClauseNotImplemented "MKWIthClause"
  convertClause (MkImpossible fc lhs) = MkDClauseNotImplemented  "MkIMpossible"

  convertField : IS.PField -> DField
  convertField (MkField fc doc x y z ty) = MkDField doc (convertName z) (convertTerm ty)

  convertTypeDecl : IS.PTypeDecl -> DTypeDecl
  convertTypeDecl (MkPTy fc nfc n doc type) = MkDTy (convertName n) doc (convertTerm type)

  convertDataDecl : IS.PDataDecl -> DDataDecl
  convertDataDecl (MkPData fc tyname tycon opts datacons)
    = MkDData (convertName tyname) (convertTerm tycon) (map convertTypeDecl datacons)
--  convertDataDecl (MkPLater fc tyname tycon) = MkDLater (convertName tyname) (convertTerm tycon)
  convertDataDecl p@(MkPLater fc tyname tycon) = MkDDataNotImplemented ("MkPLater:" ++ show tyname)

  convertNamespapce : NS.Namespace -> APIDef.Namespace
  convertNamespapce ns = DMkNS (unsafeUnfoldNamespace ns)
  convertModuleIdent : NS.ModuleIdent -> APIDef.ModuleIdent
  convertModuleIdent mi = DMkMI (unsafeUnfoldModuleIdent mi)

  export
  convertDecl : PDecl -> DDecl
  convertDecl p@(PClaim fc x y xs z) = DClaim (convertTypeDecl z)
  convertDecl p@(PDef fc xs) = DDef (map convertClause xs)
  convertDecl p@(PData fc doc x y) = DData doc (convertDataDecl y)
  convertDecl p@(PRecord fc doc v n ps con fs)  = DRecord doc (convertName n) (convertName <$> con) (map convertField fs)
  convertDecl p@(PMutual fc xs) = DDeclNotImplemented "desugarDecl removes DMutual"
  convertDecl p@(PNamespace fc ns pd) = DNamespace (convertNamespapce ns) (map convertDecl pd)
  convertDecl p = DDeclNotImplemented ""

desugarDecl : PDecl -> List PDecl
desugarDecl (PMutual fc ds) = concatMap desugarDecl ds
desugarDecl p = [p]

{-
  desugarDecl ps (PMutual fc ds)
      = do let mds = mapMaybe (getDecl AsType) ds ++ mapMaybe (getDecl AsDef) ds
           mds' <- traverse (desugarDecl ps) mds
           pure (concat mds')
-}
desugar : PDecl -> List PDecl
desugar = desugarDecl

rule : Grammar Token False Module
rule = prog "()"

moduleToDataDefs : Module ->  List APIDef.DDecl
moduleToDataDefs (MkModule headerloc moduleNS imports documentation decls) = map convertDecl . concatMap desugar $ decls

isKnownType : {ty : Type} -> {v : ty} -> (Type, ty) -> Bool
isKnownType (DDecl, y) = True
isKnownType (x, y) = False

hsDef : String -> PP.Doc ann -> PP.Doc ann
hsDef name d = pretty "{-# LANGUAGE OverloadedStrings #-}" <+> hardline <+>
               pretty "module API where" <+> hardline <+>
               pretty "import Language.APIDef" <+> hardline <+>
               pretty name <++> pretty ":: [(ModuleIdent, [DDecl])]" <+> hardline <+> pretty name <++> equals <++> d

data Path : Type where
  Abs : List String -> Path
  Rel : List String -> Path
  NoPath : Path

Show Path where
  show (Abs xs) = "Abs:" ++ show xs
  show (Rel xs) = "Rel:" ++ show xs
  show NoPath = "NoPath"

splitBy : (Char -> Bool) -> String -> List String -> List String
splitBy _ "" ls = ls
splitBy p s ls = if length (snd pair) == 0 then (fst pair) :: ls else splitBy p (S.drop 1 (snd pair)) ((fst pair)::ls)
  where
    pair : (String, String)
    pair = break p s

path : String -> Path
path "" = NoPath
path s = if isPrefixOf "/" s then Abs (drop 1 ls) else Rel ls
  where
    pref : Bool
    pref = isPrefixOf "/" s
    ls : List String
    ls = reverse $ splitBy (== '/') s []

chgs : String -> List String -> List String
chgs t [] = []
chgs t [x] = [fst pair ++ "." ++ t]
  where
    pair : (String, String)
    pair = break (== '.') x
chgs t (x :: xs) = x :: chgs t xs

changeSuffix : String -> Path -> Path
changeSuffix to (Abs xs) = Abs (chgs to xs)
changeSuffix to (Rel xs) = Rel (chgs to xs)
changeSuffix _ NoPath = NoPath

mkPath : Path -> Maybe String
mkPath (Abs xs) = Just $ "/" ++ concat (intersperse "/" xs)
mkPath (Rel xs) = Just $ concat (intersperse "/" xs)
mkPath NoPath = Nothing

(</>) : Path -> Path -> Path
(</>) p q@(Abs xs) = q
(</>) (Abs ys) (Rel xs) = Abs (ys ++ xs)
(</>) (Rel ys) (Rel xs) = Rel (ys ++ xs)
(</>) NoPath r@(Rel xs) = r
(</>) p NoPath = p

readModule : Path -> Path -> IO (Either String Module)
readModule pref p@(Rel _) = do
  let (Just p1) = mkPath $ pref </> changeSuffix "idr" p
     | _ => pure $ Left "path"
  p1Exists <- exists p1
  let (Just p2) = mkPath $ pref </> changeSuffix "lidr" p
     | _ => pure $ Left "path"
  p2Exists <- exists p2
  let p = if p2Exists then p2 else p1
  Right contents <- do
                    putStrLn p
                    readFile p
    | Left _ => pure $ Left $ "file read error:"  ++ p
  let Right (m@(MkModule headerloc moduleNS imports documentation decls)) = PS.runParser "" (isLitFile p) contents rule
    | Left e => pure $ Left "API spec format error"

  pure $ Right m

readModule _ _ = pure $ Left "Abs path not supported"

readModules : Path -> List Path -> IO (List(NS.ModuleIdent, List PDecl))
readModules _ [] = pure []
readModules pref (f :: xs) = do
  Right p@(MkModule headerloc ns imports documentation decls) <- readModule pref f
    | Left _ => pure []
  ps <- readModules pref xs
  pure $ (ns, decls) :: ps

{-
writeAST : String -> List DDecl -> IO ()
writeAST file decls =
  do
    let
--      val : (List String, List DDecl)
--      val = (unsafeUnfoldModuleIdent moduleNS, moduleToDataDefs m)
      str : String
      str = renderString . layoutPretty defaultLayoutOptions . hsDef "apiDef" $ pretty {ann = ()} decls
    Right f <- do
               putStrLn file
               openFile file WriteTruncate
      | Left _ => pure ()
    fPutStrLn f str
    closeFile f
-}

convPDecl : (NS.ModuleIdent, List PDecl) -> (APIDef.ModuleIdent, List DDecl)
convPDecl (mi, decls) = (convertModuleIdent mi, map convertDecl . concatMap desugar $ decls)
--convPDecl : (NS.ModuleIdent, List PDecl) -> (List DDecl)
--convPDecl (mi, decls) = (map convertDecl . concatMap desugar $ decls)
--convPDecl : (NS.ModuleIdent, List PDecl) -> (APIDef.ModuleIdent)
--convPDecl (mi, decls) = (convertModuleIdent mi)

main : IO ()
main = do
          [bin, spec_dir, api_file, hs_api_file]  <- getArgs
            | _ => putStrLn "too many arguments"

          Right contents <- readFile api_file
            | Left _ => putStr $ "Read file error:" ++ api_file
          let Right m@(MkModule headerloc moduleNS imports documentation decls)  = runParser "" Nothing contents (prog "()")
              | Left e => putStrLn "API spec format error"
          let idrisFiles = map (Rel . reverse . unsafeUnfoldModuleIdent . path) imports
          decls <- readModules (Rel [spec_dir]) idrisFiles

          let
            str = renderString . layoutPretty defaultLayoutOptions . hsDef "apiDefs" $ pretty {ann = ()}
                $  map convPDecl decls

          Right f <- do
                     putStrLn hs_api_file
                     openFile hs_api_file WriteTruncate
            | Left _ => putStrLn "open failed"
          Right r <- fPutStrLn f str
            | _ => pure ()
          closeFile f
          pure ()


text:
> module Predicates

> import Prelude.Maybe
> import Data.Fin
> import Control.Isomorphism

> import Sigma.Sigma

> %default total
> %access public export

> ||| Notion of finiteness for types
> Finite : Type -> Type
> Finite A = Sigma Nat (\ n => Iso A (Fin n))

> Finite0 : Type -> Type
> Finite0 = Finite

> Finite1 : {A : Type} -> (P : A -> Type) -> Type
> Finite1 {A} P = (a : A) -> Finite0 (P a)

> {-

This definition requires an exact cardinality |n| which may be
difficult to compute. But it is enough to know a finite bound, so an
alternative definition which may be more convenient is the following:

> FiniteSub : Type -> Type
> FiniteSub A = Exists (\ n => EmbProj A (Fin n))

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

> FiniteN : Nat -> Type -> Type
> FiniteN n A = Iso A (Fin n)

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Control.Algebra.ZZVerifiedInstances
-- We will forego treating this as Control.Algebra.NumericVerifiedInstances

import Data.ZZ
import Control.Algebra
import Classes.Verified
import Control.Algebra.NumericInstances

%default total

-- These can be proven through an isomorphism with the free ring on the empty type.

monoidNeutralIsNeutralL_ZZ : (l : ZZ) -> l <+> Algebra.neutral = l
monoidNeutralIsNeutralL_ZZ (Pos n) = cong {f=Pos} $ plusZeroRightNeutral n
monoidNeutralIsNeutralL_ZZ (NegS n) = Refl

monoidNeutralIsNeutralR_ZZ : (r : ZZ) -> Algebra.neutral <+> r = r
monoidNeutralIsNeutralR_ZZ (Pos n) = cong {f=Pos} $ plusZeroLeftNeutral n
monoidNeutralIsNeutralR_ZZ (NegS n) = Refl

negPlusNegnatToNegnatPlus : (l, r : Nat) -> (NegS l) <+> negNat r = negNat $ S $ l `plus` r
negPlusNegnatToNegnatPlus l Z = rewrite plusZeroRightNeutral l in Refl
negPlusNegnatToNegnatPlus l (S predr) = cong {f=NegS} $ plusSuccRightSucc l predr

onePlusMinusNatReduction : (a, b : Nat) -> Pos 1 <+> minusNatZ a (S b) = minusNatZ a b
onePlusMinusNatReduction Z b = Refl
onePlusMinusNatReduction (S preda) Z = Refl
onePlusMinusNatReduction (S preda) (S predb) = onePlusMinusNatReduction preda predb

plusNegOneMinusNatProduction : (a, b : Nat) -> minusNatZ a b <+> NegS 0 = minusNatZ a (S b)
plusNegOneMinusNatProduction Z Z = Refl
plusNegOneMinusNatProduction Z (S predb) = rewrite plusZeroRightNeutral predb in Refl
plusNegOneMinusNatProduction (S preda) Z = Refl
plusNegOneMinusNatProduction (S preda) (S predb) = plusNegOneMinusNatProduction preda predb

abelianGroupOpIsCommutative_ZZ : (l, r : ZZ) -> l <+> r = r <+> l
abelianGroupOpIsCommutative_ZZ (Pos n) (Pos m) = cong $ plusCommutative _ _
abelianGroupOpIsCommutative_ZZ (NegS n) (NegS m) = cong {f=NegS . S} $ plusCommutative _ _
abelianGroupOpIsCommutative_ZZ (Pos n) (NegS m) = Refl
abelianGroupOpIsCommutative_ZZ (NegS n) (Pos m) = Refl

total
semigroupOpIsAssociative_ZZ : (l, c, r : ZZ) -> l <+> (c <+> r) = l <+> c <+> r
semigroupOpIsAssociative_ZZ (Pos l) (Pos c) (Pos r) = cong $ plusAssociative _ _ _
semigroupOpIsAssociative_ZZ (Pos l) (Pos Z) (NegS r) = rewrite plusZeroRightNeutral l in Refl
semigroupOpIsAssociative_ZZ (Pos l) (Pos (S predc)) (NegS Z) = rewrite sym $ plusSuccRightSucc l predc in Refl
semigroupOpIsAssociative_ZZ (Pos l) (Pos (S predc)) (NegS (S predr)) = rewrite sym $ plusSuccRightSucc l predc in assert_total $ semigroupOpIsAssociative_ZZ (Pos l) (Pos predc) (NegS predr)
semigroupOpIsAssociative_ZZ (Pos l) (NegS Z) (Pos Z) = sym $ monoidNeutralIsNeutralL_ZZ _
semigroupOpIsAssociative_ZZ (Pos Z) (NegS Z) (Pos (S predr)) = Refl
semigroupOpIsAssociative_ZZ (Pos (S predl)) (NegS Z) (Pos (S predr)) = rewrite plusSuccRightSucc predl predr in Refl
semigroupOpIsAssociative_ZZ (Pos Z) (NegS (S predc)) (Pos r) = monoidNeutralIsNeutralR_ZZ _
semigroupOpIsAssociative_ZZ (Pos (S predl)) (NegS (S predc)) (Pos Z) = sym $ monoidNeutralIsNeutralL_ZZ _
semigroupOpIsAssociative_ZZ (Pos l) (NegS (S predc)) (Pos (S predr)) = trans (assert_total $ semigroupOpIsAssociative_ZZ (Pos l) (NegS predc) (Pos predr))
	$ trans (cong {f=(<+> Pos predr)}
		$ trans (sym $ onePlusMinusNatReduction l (S predc))
		$ abelianGroupOpIsCommutative_ZZ (Pos 1) (minusNatZ l $ S $ S predc))
	$ sym $ assert_total $ semigroupOpIsAssociative_ZZ _ (Pos 1) (Pos predr)
semigroupOpIsAssociative_ZZ (Pos Z) (NegS c) (NegS r) = Refl
semigroupOpIsAssociative_ZZ (Pos (S predl)) (NegS Z) (NegS r) = Refl
semigroupOpIsAssociative_ZZ (Pos (S predl)) (NegS (S predc)) (NegS r) = assert_total $ semigroupOpIsAssociative_ZZ (Pos predl) (NegS predc) (NegS r)
semigroupOpIsAssociative_ZZ (NegS l) (Pos Z) (Pos r) = Refl
semigroupOpIsAssociative_ZZ (NegS Z) (Pos (S predc)) (Pos r) = Refl
semigroupOpIsAssociative_ZZ (NegS (S predl)) (Pos (S predc)) (Pos r) = assert_total $ semigroupOpIsAssociative_ZZ (NegS predl) (Pos predc) (Pos r)
semigroupOpIsAssociative_ZZ (NegS l) (Pos Z) (NegS Z) = Refl
semigroupOpIsAssociative_ZZ (NegS l) (Pos Z) (NegS (S predr)) = Refl
semigroupOpIsAssociative_ZZ (NegS l) (Pos (S predc)) (NegS Z) = sym $ plusNegOneMinusNatProduction predc l
{-
* Recurses to case [ (NegS l) (Pos predc) (NegS predr) ]
* Depends on cases for [ x (NegS 0) (NegS predr) ]
-}
semigroupOpIsAssociative_ZZ (NegS l) (Pos (S predc)) (NegS (S predr)) = trans (assert_total $ semigroupOpIsAssociative_ZZ (NegS l) (Pos predc) (NegS predr))
	$ trans (cong {f=flip plusZ $ NegS predr} $ sym $ plusNegOneMinusNatProduction predc l)
	$ sym $ assert_total $ semigroupOpIsAssociative_ZZ ((NegS l)<+>(Pos (S predc))) (NegS 0) (NegS predr)
semigroupOpIsAssociative_ZZ (NegS l) (NegS Z) (Pos Z) = Refl
semigroupOpIsAssociative_ZZ (NegS l) (NegS Z) (Pos (S predr)) = rewrite plusZeroRightNeutral l in Refl
semigroupOpIsAssociative_ZZ (NegS l) (NegS c) (Pos Z) = Refl
semigroupOpIsAssociative_ZZ (NegS l) (NegS (S predc)) (Pos (S predr)) = rewrite sym $ plusSuccRightSucc l predc in assert_total $ semigroupOpIsAssociative_ZZ (NegS l) (NegS predc) (Pos predr)
semigroupOpIsAssociative_ZZ (NegS l) (NegS c) (NegS r) = rewrite sym $ plusSuccRightSucc l (c+r) in cong {f=NegS . S . S} $ plusAssociative l c r

minusNatZSelfZ : (n : Nat) -> minusNatZ n n = Pos 0
minusNatZSelfZ Z = Refl
minusNatZSelfZ (S predn) = minusNatZSelfZ predn

groupInverseIsInverseL_ZZ : (l : ZZ) -> l <+> inverse l = Algebra.neutral
groupInverseIsInverseL_ZZ (Pos Z) = Refl
groupInverseIsInverseL_ZZ (Pos (S predn)) = trans (cong {f=minusNatZ predn} $ multOneRightNeutral predn) $ minusNatZSelfZ predn
groupInverseIsInverseL_ZZ (NegS n) = trans (cong {f=flip minusNatZ n} $ multOneRightNeutral n) $ minusNatZSelfZ n

groupInverseIsInverseR_ZZ : (r : ZZ) -> inverse r <+> r = Algebra.neutral
groupInverseIsInverseR_ZZ (Pos Z) = Refl
groupInverseIsInverseR_ZZ (Pos (S predn)) = trans (cong {f=minusNatZ predn} $ multOneRightNeutral predn) $ minusNatZSelfZ predn
groupInverseIsInverseR_ZZ (NegS n) = trans (cong {f=flip minusNatZ n} $ multOneRightNeutral n) $ minusNatZSelfZ n

multZPosZRightZero : (left : ZZ) -> multZ left (Pos 0) = Pos 0
multZPosZRightZero (Pos n) = cong {f=Pos} $ multZeroRightZero _
multZPosZRightZero (NegS n) = cong {f=negNat} $ multZeroRightZero _

multZPosZLeftZero : (right : ZZ) -> multZ (Pos 0) right = Pos 0
multZPosZLeftZero (Pos n) = Refl
multZPosZLeftZero (NegS n) = Refl

ringOpIsAssociative_ZZ : (l, c, r : ZZ) -> l <.> (c <.> r) = l <.> c <.> r
ringOpIsAssociative_ZZ (Pos l) (Pos c) (Pos r) = cong $ multAssociative _ _ _
ringOpIsAssociative_ZZ (NegS l) (Pos Z) (Pos r) = rewrite cong {f=negNat} $ multZeroRightZero l in Refl
ringOpIsAssociative_ZZ (NegS l) (Pos c) (Pos Z) = trans (rewrite multZeroRightZero c in rewrite multZeroRightZero l in Refl) $ sym $ multZPosZRightZero _
ringOpIsAssociative_ZZ (NegS l) (Pos (S predc)) (Pos (S predr)) = cong {f=negNat} $ multAssociative (S l) (S predc) (S predr)
ringOpIsAssociative_ZZ (NegS l) (NegS c) (Pos Z) = rewrite multZeroRightZero c in trans (cong {f=negNat} $ multZeroRightZero l) $ cong {f=Pos} $ sym $ multZeroRightZero $ _
ringOpIsAssociative_ZZ (NegS l) (NegS c) (Pos (S predr)) = cong {f=Pos} $ multAssociative (S l) (S c) (S predr)
ringOpIsAssociative_ZZ (NegS l) (Pos Z) (NegS r) = rewrite multZeroRightZero l in Refl
ringOpIsAssociative_ZZ (NegS l) (Pos (S predc)) (NegS r) = cong {f=Pos} $ multAssociative (S l) (S predc) (S r)
ringOpIsAssociative_ZZ (NegS l) (NegS c) (NegS r) = cong {f=negNat} $ multAssociative (S l) (S c) (S r)
ringOpIsAssociative_ZZ (Pos Z) (NegS c) (Pos r) = multZPosZLeftZero _
ringOpIsAssociative_ZZ (Pos l) (NegS c) (Pos Z) = rewrite multZeroRightZero c in trans (multZPosZRightZero (Pos l)) $ sym $ multZPosZRightZero _
ringOpIsAssociative_ZZ (Pos (S predl)) (NegS c) (Pos (S predr)) = cong {f=negNat} $ multAssociative (S predl) (S c) (S predr)
ringOpIsAssociative_ZZ (Pos Z) (Pos c) (NegS r) = multZPosZLeftZero _
ringOpIsAssociative_ZZ (Pos l) (Pos Z) (NegS r) = rewrite (multZeroRightZero l) in Refl
ringOpIsAssociative_ZZ (Pos (S predl)) (Pos (S predc)) (NegS r) = cong {f=negNat} $ multAssociative (S predl) (S predc) (S r)
ringOpIsAssociative_ZZ (Pos Z) (NegS c) (NegS r) = Refl
ringOpIsAssociative_ZZ (Pos (S predl)) (NegS c) (NegS r) = cong {f=Pos} $ multAssociative (S predl) (S c) (S r)

negativeIsNegOneTimesRight : (right : ZZ) -> inverse right = (inverse Algebra.unity) <.> right
negativeIsNegOneTimesRight (Pos r) = cong {f=negNat} $ trans (multOneRightNeutral r) $ sym $ plusZeroRightNeutral r
negativeIsNegOneTimesRight (NegS r) = cong {f=Pos . S} $ trans (multOneRightNeutral r) $ sym $ plusZeroRightNeutral r

minusNatZNegOneTimesFlip : multZ (NegS 0) $ minusNatZ a b = minusNatZ b a
minusNatZNegOneTimesFlip {a=Z} {b=Z} = Refl
minusNatZNegOneTimesFlip {a=Z} {b=S predb} = cong {f=Pos . S} $ plusZeroRightNeutral predb
minusNatZNegOneTimesFlip {a=S preda} {b=Z} = cong {f=NegS} $ plusZeroRightNeutral preda
minusNatZNegOneTimesFlip {a=S preda} {b=S predb} = minusNatZNegOneTimesFlip {a=preda} {b=predb}

negOneDistributesL_ZZ : (c, r : ZZ) -> (inverse Algebra.unity) <.> (c <+> r) = (inverse Algebra.unity)<.>c <+> (inverse Algebra.unity)<.>r
negOneDistributesL_ZZ (Pos Z) r = rewrite monoidNeutralIsNeutralR_ZZ (NegS 0 <.> r) in rewrite monoidNeutralIsNeutralR_ZZ r in Refl
negOneDistributesL_ZZ (Pos (S predc)) (Pos Z) = rewrite plusZeroRightNeutral predc in rewrite plusZeroRightNeutral predc in Refl
negOneDistributesL_ZZ (Pos (S predc)) (Pos (S predr)) = rewrite plusZeroRightNeutral predr in rewrite plusZeroRightNeutral predc in rewrite plusZeroRightNeutral (predc+(S predr)) in cong {f=NegS} $ sym $ plusSuccRightSucc predc predr
negOneDistributesL_ZZ (Pos (S Z)) (NegS Z) = Refl
negOneDistributesL_ZZ (Pos (S $ S predc)) (NegS Z) = Refl
negOneDistributesL_ZZ (Pos (S predc)) (NegS (S predr)) = trans minusNatZNegOneTimesFlip $ rewrite plusZeroRightNeutral predc in rewrite plusZeroRightNeutral predr in Refl
negOneDistributesL_ZZ (NegS c) (Pos Z) = rewrite plusZeroRightNeutral c in rewrite plusZeroRightNeutral c in Refl
negOneDistributesL_ZZ (NegS c) (Pos (S predr)) = rewrite plusZeroRightNeutral c in rewrite plusZeroRightNeutral predr in minusNatZNegOneTimesFlip
negOneDistributesL_ZZ (NegS c) (NegS r) = cong {f=Pos . S} $ rewrite plusZeroRightNeutral (c+r) in rewrite plusZeroRightNeutral c in rewrite plusZeroRightNeutral r in plusSuccRightSucc c r

total
ringOpIsDistributiveL_ZZ : ( l, c, r : ZZ ) -> l <.> (c <+> r) = l <.> c <+> l <.> r
ringOpIsDistributiveL_ZZ (Pos l) (Pos c) (Pos r) = cong {f=Pos} $ multDistributesOverPlusRight _ _ _
ringOpIsDistributiveL_ZZ (NegS l) (Pos Z) (Pos r) = rewrite (multZeroRightZero l) in sym $ plusZeroLeftNeutralZ _
ringOpIsDistributiveL_ZZ (NegS l) (Pos (S predc)) (Pos r) = trans (cong {f=negNat} $ multDistributesOverPlusRight (S l) (S predc) r) $ sym $ negPlusNegnatToNegnatPlus _ _
ringOpIsDistributiveL_ZZ (Pos l) (NegS c) (Pos Z) = rewrite multZeroRightZero l in sym $ plusZeroRightNeutralZ _
-- if (r) is a successor, induce from the theorem on its predecessor.
ringOpIsDistributiveL_ZZ (Pos l) (NegS c) (Pos (S predr)) = trans (trans (cong $ sym $ onePlusMinusNatReduction predr c) $
	trans (assert_total $ ringOpIsDistributiveL_ZZ (Pos l) (Pos 1) (minusNatZ predr (S c))) $ rewrite multOneRightNeutral l in Refl)
	$ trans (cong {f=((Pos l)<+>)} $ assert_total $ ringOpIsDistributiveL_ZZ (Pos l) (NegS c) (Pos predr))
	$ trans (semigroupOpIsAssociative_ZZ (Pos l) (negNat $ mult l $ S c) $ Pos $ mult l predr)
	$ trans ( trans (cong {f=flip plusZ $ Pos $ mult l predr} $ abelianGroupOpIsCommutative_ZZ (Pos l) (negNat $ mult l $ S c))
		$ sym $ semigroupOpIsAssociative_ZZ (negNat $ mult l $ S c) (Pos l) (Pos $ mult l predr))
	$ cong {f=(plusZ $ negNat $ mult l $ S c) . Pos}
		$ trans (cong {f=flip plus $ mult l predr} $ sym $ multOneRightNeutral l)
		$ sym $ multDistributesOverPlusRight l 1 predr
-- reduces to 3 and the special case (negOneDistributesL_ZZ)
ringOpIsDistributiveL_ZZ (NegS l) (NegS c) (Pos r) = trans (cong {f=(flip multZ $ minusNatZ r $ S c) . NegS} $ sym $ plusZeroRightNeutral l)
	$ trans (sym $ ringOpIsAssociative_ZZ (inverse Algebra.unity) (Pos (S l)) $ minusNatZ r (S c))
	$ trans (cong {f=multZ $ inverse unity} $ assert_total $ ringOpIsDistributiveL_ZZ (Pos (S l)) (NegS c) (Pos r))
	$ trans (negOneDistributesL_ZZ (Pos (S l) <.> NegS c) (Pos (S l) <.> Pos r))
	$ trans (cong $ sym $ negativeIsNegOneTimesRight (Pos (S l) <.> Pos r))
	$ trans (cong {f=(flip plusZ $ negNat (mult (plus r (mult l r)) 1)) . Pos . S} $ plusZeroRightNeutral _)
	$ cong {f=plusZ $ Pos $ S $ plus c $ mult l $ S c} $ cong {f=negNat} $ multOneRightNeutral _
-- reduces to 3
ringOpIsDistributiveL_ZZ (Pos l) (Pos c) (NegS r) = trans (cong {f=((Pos l) <.>)} $ abelianGroupOpIsCommutative_ZZ (Pos c) (NegS r))
	$ trans (assert_total $ ringOpIsDistributiveL_ZZ (Pos l) (NegS r) (Pos c))
	$ abelianGroupOpIsCommutative_ZZ ((Pos l)<.>(NegS r)) ((Pos l)<.>(Pos c))
-- reduces to 4
ringOpIsDistributiveL_ZZ (NegS l) (Pos c) (NegS r) = trans (cong {f=((NegS l) <.>)} $ abelianGroupOpIsCommutative_ZZ (Pos c) (NegS r))
	$ trans (assert_total $ ringOpIsDistributiveL_ZZ (NegS l) (NegS r) (Pos c))
	$ abelianGroupOpIsCommutative_ZZ ((NegS l)<.>(NegS r)) ((NegS l)<.>(Pos c))
ringOpIsDistributiveL_ZZ (Pos Z) (NegS c) (NegS r) = Refl
ringOpIsDistributiveL_ZZ (Pos (S predl)) (NegS c) (NegS r) = cong {f=NegS . S}
	$ trans (cong
		$ trans (cong $ plusSuccRightSucc (S c) r)
		$ multDistributesOverPlusRight predl (S c) (S r))
	$ trans (sym $ plusAssociative c r _)
	$ trans (cong {f=plus c}
		$ trans (plusCommutative r _)
		$ trans (sym $ plusAssociative (mult predl $ S c) (mult predl $ S r) r)
		$ cong $ plusCommutative _ r)
	$ plusAssociative c (mult predl $ S c) $ plus r $ mult predl $ S r
-- Reduces to 7 and the special case (negOneDistributesL_ZZ)
-- mirrors the proof of case [(NegS l) (NegS c) (Pos r)].
ringOpIsDistributiveL_ZZ (NegS l) (NegS c) (NegS r) = trans (rewrite sym $ plusZeroRightNeutral l in Refl)
	-- THIS LINE HERE IS CLEARER THAN IN case [(NegS l) (NegS c) (Pos r)]'s proof! Change (NegS r) to (Pos r).
	$ trans (sym $ ringOpIsAssociative_ZZ (inverse Algebra.unity) (Pos (S l)) $ NegS c <+> NegS r)
	$ trans (cong {f=multZ $ inverse unity} $ assert_total $ ringOpIsDistributiveL_ZZ (Pos (S l)) (NegS c) (NegS r))
	$ trans (negOneDistributesL_ZZ (Pos (S l) <.> NegS c) (Pos (S l) <.> NegS r))
	$ trans ( cong {f=plusZ (multZ (NegS 0) (Pos (S l) <.> NegS c))} $ sym $ negativeIsNegOneTimesRight (Pos (S l) <.> NegS r) )
	{-
	HERE THE PROOF IS DIFFERENT BECAUSE THE CONGs ON THE (multOneRightNeutral)
	WOULD HAVE TO BE DIFFERENT.
	-}
	$ trans (rewrite plusZeroRightNeutral $ c+l*(S c) in Refl)
	$ rewrite multOneRightNeutral (r+l*(S r)) in Refl

ringOpIsCommutative_ZZ : ( l, r : ZZ ) -> l <.> r = r <.> l
ringOpIsCommutative_ZZ (Pos l) (Pos r) = cong $ multCommutative l r
ringOpIsCommutative_ZZ (NegS l) (Pos r) = cong {f=negNat} $ multCommutative (S l) r
ringOpIsCommutative_ZZ (Pos l) (NegS r) = cong {f=negNat} $ multCommutative l (S r)
ringOpIsCommutative_ZZ (NegS l) (NegS r) = cong {f=Pos} $ multCommutative (S l) (S r)

ringOpIsDistributiveR_ZZ : ( l, c, r : ZZ ) -> (l <+> c) <.> r = l <.> r <+> c <.> r
ringOpIsDistributiveR_ZZ l c r = trans (ringOpIsCommutative_ZZ (l<+>c) r)
	$ trans (ringOpIsDistributiveL_ZZ r l c)
	$ trans (cong {f=((r<.>l) <+>)} $ ringOpIsCommutative_ZZ r c)
	$ cong {f=(<+> (c<.>r))} $ ringOpIsCommutative_ZZ r l

ringWithUnityIsUnityL_ZZ : ( l : ZZ ) -> l <.> Algebra.unity = l
ringWithUnityIsUnityL_ZZ (Pos l) = cong $ multOneRightNeutral l
ringWithUnityIsUnityL_ZZ (NegS l) = cong $ multOneRightNeutral l

ringWithUnityIsUnityR_ZZ : ( r : ZZ ) -> Algebra.unity <.> r = r
ringWithUnityIsUnityR_ZZ (Pos r) = cong $ multOneLeftNeutral r
ringWithUnityIsUnityR_ZZ (NegS r) = cong $ multOneLeftNeutral r

instance VerifiedSemigroup ZZ where
	semigroupOpIsAssociative = semigroupOpIsAssociative_ZZ

instance VerifiedMonoid ZZ where {
	monoidNeutralIsNeutralL = monoidNeutralIsNeutralL_ZZ
	monoidNeutralIsNeutralR = monoidNeutralIsNeutralR_ZZ
}

instance VerifiedGroup ZZ where {
	groupInverseIsInverseL = groupInverseIsInverseL_ZZ
	groupInverseIsInverseR = groupInverseIsInverseR_ZZ
}

instance VerifiedAbelianGroup ZZ where {
	abelianGroupOpIsCommutative = abelianGroupOpIsCommutative_ZZ
}

instance VerifiedRing ZZ where {
	ringOpIsAssociative = ringOpIsAssociative_ZZ
	ringOpIsDistributiveL = ringOpIsDistributiveL_ZZ
	ringOpIsDistributiveR = ringOpIsDistributiveR_ZZ
}

instance VerifiedRingWithUnity ZZ where {
	ringWithUnityIsUnityL = ringWithUnityIsUnityL_ZZ
	ringWithUnityIsUnityR = ringWithUnityIsUnityR_ZZ
}

ext: idr


text:
module Utils.Base64

import Control.Monad.Trans
import Data.Bits
import Data.List
import Data.String.Parser
import Data.Vect
import Utils.Bytes
import Utils.Misc

alphabets : Vect 64 Char
alphabets = fromList $ unpack "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"

padding : Char
padding = '='

base64_chr : Monad m => ParseT m (Fin 64)
base64_chr = do
  c <- satisfy $ const True
  case elemIndex c alphabets of
    Just i => pure i
    Nothing => fail $ "invalid base64 character: " <+> show c

export
is_base64_char : Char -> Bool
is_base64_char c = isAlphaNum c || (c == '+') || (c == '/') || (c == '=')

many_to_bits8 : List Bits8 -> Either String (List Bits8)
many_to_bits8 [] = Right []
many_to_bits8 [x] = Left "underfed, not enough base64 chars"
many_to_bits8 [a, b] = Right [ (shiftL a 2) .|. (shiftR b 4) ]
many_to_bits8 [a, b, c] = Right [ (shiftL a 2) .|. (shiftR b 4), (shiftL b 4) .|. (shiftR c 2) ]
many_to_bits8 (a :: b :: c :: d :: xs) = map (four_to_three a b c d <+>) (many_to_bits8 xs)
  where
    four_to_three : Bits8 -> Bits8 -> Bits8 -> Bits8 -> List Bits8
    four_to_three a b c d = [(shiftL a 2) .|. (shiftR b 4), (shiftL b 4) .|. (shiftR c 2), (shiftL (c .&. 0b11) 6) .|. d]

parse_base64 : Monad m => ParseT m (List Bits8)
parse_base64 = do
  alphas <- many base64_chr
  _ <- many (char padding)
  case many_to_bits8 (cast . finToInteger <$> alphas) of
    Right x => pure x
    Left err => fail err

three_to_four : Bits8 -> Bits8 -> Bits8 -> List Char
three_to_four a b c =
  let i = shiftR a 2
      j = (shiftL (a .&. 0b11) 4) .|. (shiftR b 4)
      k = (shiftL (b .&. 0b1111) 2) .|. (shiftR c 6)
      l = c .&. 0b111111
      ijkl =
        [ modFinNZ (cast i) 64 SIsNonZero
        , modFinNZ (cast j) 64 SIsNonZero
        , modFinNZ (cast k) 64 SIsNonZero
        , modFinNZ (cast l) 64 SIsNonZero
        ]
  in (\x => index x alphabets) <$> ijkl

bits8_to_many : List Bits8 -> List Char
bits8_to_many [] = []
bits8_to_many [a] = (take 2 $ three_to_four a 0 0) <+> [padding, padding]
bits8_to_many [a, b] = (take 3 $ three_to_four a b 0) <+> [padding]
bits8_to_many (a :: b :: c :: xs) = three_to_four a b c <+> bits8_to_many xs

export
base64_decode : String -> Either String (List Bits8)
base64_decode = map fst . parse parse_base64

export
base64_encode : List Bits8 -> String
base64_encode = pack . bits8_to_many


text:
module Core.Normalise.Eval

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Options
import Core.Primitives
import Core.TT
import Core.Value

import Libraries.Data.IntMap
import Data.List
import Data.Maybe
import Data.Nat
import Data.Vect

%default covering

-- A pair of a term and its normal form. This could be constructed either
-- from a term (via 'gnf') or a normal form (via 'glueBack') but the other
-- part will only be constructed when needed, because it's in Core.
public export
data Glued : List Name -> Type where
     MkGlue : (fromTerm : Bool) -> -- is it built from the term; i.e. can
                                   -- we read the term straight back?
              Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars

export
isFromTerm : Glued vars -> Bool
isFromTerm (MkGlue ft _ _) = ft

export
getTerm : Glued vars -> Core (Term vars)
getTerm (MkGlue _ tm _) = tm

export
getNF : {auto c : Ref Ctxt Defs} -> Glued vars -> Core (NF vars)
getNF {c} (MkGlue _ _ nf) = nf c

Stack : List Name -> Type
Stack vars = List (FC, Closure vars)

evalWithOpts : {auto c : Ref Ctxt Defs} ->
               {free, vars : _} ->
               Defs -> EvalOpts ->
               Env Term free -> LocalEnv free vars ->
               Term (vars ++ free) -> Stack free -> Core (NF free)

export
evalClosure : {auto c : Ref Ctxt Defs} ->
              {free : _} -> Defs -> Closure free -> Core (NF free)

export
evalArg : {auto c : Ref Ctxt Defs} -> {free : _} -> Defs -> Closure free -> Core (NF free)
evalArg defs c = evalClosure defs c

export
toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer
toClosure opts env tm = MkClosure opts [] env tm

updateLimit : NameType -> Name -> EvalOpts -> Core (Maybe EvalOpts)
updateLimit Func n opts
    = pure $ if isNil (reduceLimit opts)
         then Just opts
         else case lookup n (reduceLimit opts) of
                   Nothing => Nothing
                   Just Z => Nothing
                   Just (S k) =>
                      Just (record { reduceLimit $= set n k } opts)
  where
    set : Name -> Nat -> List (Name, Nat) -> List (Name, Nat)
    set n v [] = []
    set n v ((x, l) :: xs)
        = if x == n
             then (x, v) :: xs
             else (x, l) :: set n v xs
updateLimit t n opts = pure (Just opts)

data CaseResult a
     = Result a
     | NoMatch -- case alternative didn't match anything
     | GotStuck -- alternative matched, but got stuck later

parameters (defs : Defs, topopts : EvalOpts)
  mutual
    eval : {auto c : Ref Ctxt Defs} ->
           {free, vars : _} ->
           Env Term free -> LocalEnv free vars ->
           Term (vars ++ free) -> Stack free -> Core (NF free)
    eval env locs (Local fc mrig idx prf) stk
        = evalLocal env fc mrig idx prf stk locs
    eval env locs (Ref fc nt fn) stk
        = evalRef env False fc nt fn stk (NApp fc (NRef nt fn) stk)
    eval {vars} {free} env locs (Meta fc name idx args) stk
        = evalMeta env fc name idx (closeArgs args) stk
      where
        -- Yes, it's just a map, but specialising it by hand since we
        -- use this a *lot* and it saves the run time overhead of making
        -- a closure and calling APPLY.
        closeArgs : List (Term (vars ++ free)) -> List (Closure free)
        closeArgs [] = []
        closeArgs (t :: ts) = MkClosure topopts locs env t :: closeArgs ts
    eval env locs (Bind fc x (Lam _ r _ ty) scope) (thunk :: stk)
        = eval env (snd thunk :: locs) scope stk
    eval env locs (Bind fc x b@(Let _ r val ty) scope) stk
        = if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)
             then do let b' = map (MkClosure topopts locs env) b
                     pure $ NBind fc x b'
                        (\defs', arg => evalWithOpts defs' topopts
                                                env (arg :: locs) scope stk)
             else eval env (MkClosure topopts locs env val :: locs) scope stk
    eval env locs (Bind fc x b scope) stk
        = do let b' = map (MkClosure topopts locs env) b
             pure $ NBind fc x b'
                      (\defs', arg => evalWithOpts defs' topopts
                                              env (arg :: locs) scope stk)
    eval env locs (App fc fn arg) stk
        = case strategy topopts of
               CBV => do arg' <- eval env locs arg []
                         eval env locs fn ((fc, MkNFClosure topopts env arg') :: stk)
               CBN => eval env locs fn ((fc, MkClosure topopts locs env arg) :: stk)
    eval env locs (As fc s n tm) stk
        = if removeAs topopts
             then eval env locs tm stk
             else do n' <- eval env locs n stk
                     tm' <- eval env locs tm stk
                     pure (NAs fc s n' tm')
    eval env locs (TDelayed fc r ty) stk
        = do ty' <- eval env locs ty stk
             pure (NDelayed fc r ty')
    eval env locs (TDelay fc r ty tm) stk
        = pure (NDelay fc r (MkClosure topopts locs env ty)
                            (MkClosure topopts locs env tm))
    eval env locs (TForce fc r tm) stk
        = do tm' <- eval env locs tm []
             case tm' of
                  NDelay fc r _ arg =>
                      eval env (arg :: locs) (Local {name = UN (Basic "fvar")} fc Nothing _ First) stk
                  _ => pure (NForce fc r tm' stk)
    eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c
    eval env locs (Erased fc i) stk = pure $ NErased fc i
    eval env locs (TType fc) stk = pure $ NType fc

    -- Apply an evaluated argument (perhaps cached from an earlier evaluation)
    -- to a stack
    applyToStack : {auto c : Ref Ctxt Defs} ->
                   {free : _} ->
                   Env Term free -> Bool ->
                   NF free -> Stack free -> Core (NF free)
    applyToStack env cont (NBind fc _ (Lam _ _ _ _) sc) (arg :: stk)
        = do arg' <- sc defs $ snd arg
             applyToStack env cont arg' stk
    applyToStack env cont (NBind fc x b@(Let _ r val ty) sc) stk
        = if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)
             then pure (NBind fc x b
                              (\defs', arg => applyToStack env cont !(sc defs' arg) stk))
             else applyToStack env cont !(sc defs val) stk
    applyToStack env cont (NBind fc x b sc) stk
        = pure (NBind fc x b
                      (\defs', arg => applyToStack env cont !(sc defs' arg) stk))
    applyToStack env cont (NApp fc (NRef nt fn) args) stk
        = evalRef env False fc nt fn (args ++ stk)
                  (NApp fc (NRef nt fn) (args ++ stk))
    applyToStack env cont (NApp fc (NLocal mrig idx p) args) stk
        = evalLocal env fc mrig _ p (args ++ stk) []
    applyToStack env cont (NApp fc (NMeta n i args) args') stk
        = evalMeta env fc n i args (args' ++ stk)
    applyToStack env cont (NDCon fc n t a args) stk
        = pure $ NDCon fc n t a (args ++ stk)
    applyToStack env cont (NTCon fc n t a args) stk
        = pure $ NTCon fc n t a (args ++ stk)
    applyToStack env cont (NAs fc s p t) stk
       = if removeAs topopts
            then applyToStack env cont t stk
            else do p' <- applyToStack env cont p []
                    t' <- applyToStack env cont t stk
                    pure (NAs fc s p' t')
    applyToStack env cont (NDelayed fc r tm) stk
       = do tm' <- applyToStack env cont tm stk
            pure (NDelayed fc r tm')
    applyToStack env cont nf@(NDelay fc r ty tm) stk
       = pure nf -- stack should always be empty here!
    applyToStack env cont (NForce fc r tm args) stk
       = do tm' <- applyToStack env cont tm []
            case tm' of
                 NDelay fc r _ arg =>
                    eval env [arg] (Local {name = UN (Basic "fvar")} fc Nothing _ First) stk
                 _ => pure (NForce fc r tm' (args ++ stk))
    applyToStack env cont nf@(NPrimVal fc _) _ = pure nf
    applyToStack env cont nf@(NErased fc _) _ = pure nf
    applyToStack env cont nf@(NType fc) _ = pure nf

    evalLocClosure : {auto c : Ref Ctxt Defs} ->
                     {free : _} ->
                     Env Term free ->
                     FC -> Maybe Bool ->
                     Stack free ->
                     Closure free ->
                     Core (NF free)
    evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')
        = evalWithOpts defs opts env' locs' tm' stk
    evalLocClosure {free} env fc mrig stk (MkNFClosure opts env' nf)
        = applyToStack env' False nf stk

    evalLocal : {auto c : Ref Ctxt Defs} ->
                {free : _} ->
                Env Term free ->
                FC -> Maybe Bool ->
                (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
                Stack free ->
                LocalEnv free vars ->
                Core (NF free)
    -- If it's one of the free variables, we are done unless the free
    -- variable maps to a let-binding
    evalLocal env fc mrig idx prf stk []
        = if not (holesOnly topopts || argHolesOnly topopts)
             -- if we know it's not a let, no point in even running `getBinder`
             && fromMaybe True mrig
             then
               case getBinder prf env of
                    Let _ _ val _ => eval env [] val stk
                    _ => pure $ NApp fc (NLocal mrig idx prf) stk
             else pure $ NApp fc (NLocal mrig idx prf) stk
    evalLocal env fc mrig Z First stk (x :: locs)
        = evalLocClosure env fc mrig stk x
    evalLocal {vars = x :: xs} {free}
              env fc mrig (S idx) (Later p) stk (_ :: locs)
        = evalLocal {vars = xs} env fc mrig idx p stk locs

    updateLocal : EvalOpts -> Env Term free ->
                  (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
                  LocalEnv free vars -> NF free ->
                  LocalEnv free vars
    updateLocal opts env Z First (x :: locs) nf
        = MkNFClosure opts env nf :: locs
    updateLocal opts env (S idx) (Later p) (x :: locs) nf
        = x :: updateLocal opts env idx p locs nf
    updateLocal _ _ _ _ locs nf = locs

    evalMeta : {auto c : Ref Ctxt Defs} ->
               {free : _} ->
               Env Term free ->
               FC -> Name -> Int -> List (Closure free) ->
               Stack free -> Core (NF free)
    evalMeta env fc nm i args stk
        = let args' = if isNil stk then map (EmptyFC,) args
                         else map (EmptyFC,) args ++ stk
                        in
              evalRef env True fc Func (Resolved i) args'
                          (NApp fc (NMeta nm i args) stk)

    -- The commented out logging here might still be useful one day, but
    -- evalRef is used a lot and even these tiny checks turn out to be
    -- worth skipping if we can
    evalRef : {auto c : Ref Ctxt Defs} ->
              {free : _} ->
              Env Term free ->
              (isMeta : Bool) ->
              FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
              Core (NF free)
    evalRef env meta fc (DataCon tag arity) fn stk def
        = do -- logC "eval.ref.data" 50 $ do fn' <- toFullNames fn -- Can't use ! here, it gets lifted too far
             --                             pure $ "Found data constructor: " ++ show fn'
             pure $ NDCon fc fn tag arity stk
    evalRef env meta fc (TyCon tag arity) fn stk def
        = do -- logC "eval.ref.type" 50 $ do fn' <- toFullNames fn
             --                             pure $ "Found type constructor: " ++ show fn'
             pure $ ntCon fc fn tag arity stk
    evalRef env meta fc Bound fn stk def
        = do -- logC "eval.ref.bound" 50 $ do fn' <- toFullNames fn
             --                              pure $ "Found bound variable: " ++ show fn'
             pure def
    evalRef env meta fc nt@Func n stk def
        = do -- logC "eval.ref.func" 50 $ do n' <- toFullNames n
             --                             pure $ "Found function: " ++ show n'
             Just res <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure def
             let redok1 = evalAll topopts
             let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
                                         (fullname res)
                                         (visibility res)
             -- want to shortcut that second check, if we're evaluating
             -- everything, so don't let bind unless we need that log!
             let redok = redok1 || redok2
             checkTimer -- If we're going to time out anywhere, it'll be
                        -- when evaluating something recursive, so this is a
                        -- good place to check
             unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n
                                                      pure $ "Stuck function: " ++ show n'
             if redok
                then do
                   Just opts' <- updateLimit nt n topopts
                        | Nothing => do log "eval.stuck" 10 $ "Function " ++ show n ++ " past reduction limit"
                                        pure def -- name is past reduction limit
                   evalDef env opts' meta fc
                           (multiplicity res) (definition res) (flags res) stk def
                else pure def

    getCaseBound : List (Closure free) ->
                   (args : List Name) ->
                   LocalEnv free more ->
                   Maybe (LocalEnv free (args ++ more))
    getCaseBound []            []        loc = Just loc
    getCaseBound []            (_ :: _)  loc = Nothing -- mismatched arg length
    getCaseBound (arg :: args) []        loc = Nothing -- mismatched arg length
    getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc

    evalConAlt : {auto c : Ref Ctxt Defs} ->
                 {more, free : _} ->
                 Env Term free ->
                 LocalEnv free more -> EvalOpts -> FC ->
                 Stack free ->
                 (args : List Name) ->
                 List (Closure free) ->
                 CaseTree (args ++ more) ->
                 Core (CaseResult (NF free))
    evalConAlt env loc opts fc stk args args' sc
         = do let Just bound = getCaseBound args' args loc
                   | Nothing => pure GotStuck
              evalTree env bound opts fc stk sc

    tryAlt : {auto c : Ref Ctxt Defs} ->
             {free, more : _} ->
             Env Term free ->
             LocalEnv free more -> EvalOpts -> FC ->
             Stack free -> NF free -> CaseAlt more ->
             Core (CaseResult (NF free))
    -- Ordinary constructor matching
    tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc)
         = if tag == tag'
              then evalConAlt env loc opts fc stk args (map snd args') sc
              else pure NoMatch
    -- Type constructor matching, in typecase
    tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc)
         = if nm == nm'
              then evalConAlt env loc opts fc stk args (map snd args') sc
              else pure NoMatch
    -- Primitive type matching, in typecase
    tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag args sc)
         = case args of -- can't just test for it in the `if` for typing reasons
             [] => if UN (Basic $ show c) == nm
                   then evalTree env loc opts fc stk sc
                   else pure NoMatch
             _ => pure NoMatch
    -- Type of type matching, in typecase
    tryAlt env loc opts fc stk (NType _) (ConCase (UN (Basic "Type")) tag [] sc)
         = evalTree env loc opts fc stk sc
    -- Arrow matching, in typecase
    tryAlt {more}
           env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN (Basic "->")) tag [s,t] sc)
       = evalConAlt {more} env loc opts fc stk [s,t]
                  [aty,
                   MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]
                  sc
    -- Delay matching
    tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)
         = evalTree env (ty :: arg :: loc) opts fc stk sc
    -- Constant matching
    tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc)
         = if c == c' then evalTree env loc opts fc stk sc
                      else pure NoMatch
    -- Default case matches against any *concrete* value
    tryAlt env loc opts fc stk val (DefaultCase sc)
         = if concrete val
              then evalTree env loc opts fc stk sc
              else pure GotStuck
      where
        concrete : NF free -> Bool
        concrete (NDCon _ _ _ _ _) = True
        concrete (NTCon _ _ _ _ _) = True
        concrete (NPrimVal _ _) = True
        concrete (NBind _ _ _ _) = True
        concrete (NType _) = True
        concrete _ = False
    tryAlt _ _ _ _ _ _ _ = pure GotStuck

    findAlt : {auto c : Ref Ctxt Defs} ->
              {args, free : _} ->
              Env Term free ->
              LocalEnv free args -> EvalOpts -> FC ->
              Stack free -> NF free -> List (CaseAlt args) ->
              Core (CaseResult (NF free))
    findAlt env loc opts fc stk val [] = do
      log "eval.casetree.stuck" 2 "Ran out of alternatives"
      pure GotStuck
    findAlt env loc opts fc stk val (x :: xs)
         = do Result val <- tryAlt env loc opts fc stk val x
                   | NoMatch => findAlt env loc opts fc stk val xs
                   | GotStuck => do
                       logC "eval.casetree.stuck" 5 $
                         pure $ "Got stuck matching " ++ show val ++ " against " ++ show !(toFullNames x)
                       pure GotStuck
              pure (Result val)

    evalTree : {auto c : Ref Ctxt Defs} ->
               {args, free : _} -> Env Term free -> LocalEnv free args ->
               EvalOpts -> FC ->
               Stack free -> CaseTree args ->
               Core (CaseResult (NF free))
    evalTree env loc opts fc stk (Case {name} idx x _ alts)
      = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
           -- we have not defined quote yet (it depends on eval itself) so we show the NF
           -- i.e. only the top-level constructor.
           log "eval.casetree" 5 $ "Evaluated " ++ show name ++ " to " ++ show xval
           let loc' = updateLocal opts env idx (varExtend x) loc xval
           findAlt env loc' opts fc stk xval alts
    evalTree env loc opts fc stk (STerm _ tm)
          = case fuel opts of
                 Nothing => do res <- evalWithOpts defs opts env loc (embed tm) stk
                               pure (Result res)
                 Just Z => pure GotStuck
                 Just (S k) =>
                      do let opts' = record { fuel = Just k } opts
                         res <- evalWithOpts defs opts' env loc (embed tm) stk
                         pure (Result res)
    evalTree env loc opts fc stk _ = pure GotStuck

    -- Take arguments from the stack, as long as there's enough.
    -- Returns the arguments, and the rest of the stack
    takeFromStack : (arity : Nat) -> Stack free ->
                    Maybe (Vect arity (Closure free), Stack free)
    takeFromStack arity stk = takeStk arity stk []
      where
        takeStk : (remain : Nat) -> Stack free ->
                  Vect got (Closure free) ->
                  Maybe (Vect (got + remain) (Closure free), Stack free)
        takeStk {got} Z stk acc = Just (rewrite plusZeroRightNeutral got in
                                    reverse acc, stk)
        takeStk (S k) [] acc = Nothing
        takeStk {got} (S k) (arg :: stk) acc
           = rewrite sym (plusSuccRightSucc got k) in
                     takeStk k stk (snd arg :: acc)

    argsFromStack : (args : List Name) ->
                    Stack free ->
                    Maybe (LocalEnv free args, Stack free)
    argsFromStack [] stk = Just ([], stk)
    argsFromStack (n :: ns) [] = Nothing
    argsFromStack (n :: ns) (arg :: args)
         = do (loc', stk') <- argsFromStack ns args
              pure (snd arg :: loc', stk')

    evalOp : {auto c : Ref Ctxt Defs} ->
             {arity, free : _} ->
             (Vect arity (NF free) -> Maybe (NF free)) ->
             Stack free -> (def : Lazy (NF free)) ->
             Core (NF free)
    evalOp {arity} fn stk def
        = case takeFromStack arity stk of
               -- Stack must be exactly the right height
               Just (args, []) =>
                  do argsnf <- evalAll args
                     pure $ case fn argsnf of
                          Nothing => def
                          Just res => res
               _ => pure def
      where
        -- No traverse for Vect in Core...
        evalAll : Vect n (Closure free) -> Core (Vect n (NF free))
        evalAll [] = pure []
        evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)

    evalDef : {auto c : Ref Ctxt Defs} ->
              {free : _} ->
              Env Term free -> EvalOpts ->
              (isMeta : Bool) -> FC ->
              RigCount -> Def -> List DefFlag ->
              Stack free -> (def : Lazy (NF free)) ->
              Core (NF free)
    evalDef env opts meta fc rigd (PMDef r args tree _ _) flags stk def
       -- If evaluating the definition fails (e.g. due to a case being
       -- stuck) return the default.
       -- We can use the definition if one of the following is true:
       --   + The 'alwayReduce' flag (r) is set
       --   + We're not in 'holesOnly', 'argHolesOnly' or 'tcInline'
       --         (that's the default mode)
       --   + It's a metavariable and not in Rig0
       --   + It's a metavariable and we're not in 'argHolesOnly'
       --   + It's inlinable and we're in 'tcInline'
        = if alwaysReduce r
             || (not (holesOnly opts || argHolesOnly opts || tcInline opts))
             || (meta && not (isErased rigd))
             || (meta && holesOnly opts)
             || (tcInline opts && elem TCInline flags)
             then case argsFromStack args stk of
                       Nothing => pure def
                       Just (locs', stk') =>
                            do Result res <- evalTree env locs' opts fc stk' tree
                                    | _ => pure def
                               pure res
             else pure def
    evalDef env opts meta fc rigd (Builtin op) flags stk def
        = evalOp (getOp op) stk def
    -- All other cases, use the default value, which is already applied to
    -- the stack
    evalDef env opts _ _ _ _ _ stk def = pure def

-- Make sure implicit argument order is right... 'vars' is used so we'll
-- write it explicitly, but it does appear after the parameters in 'eval'!
evalWithOpts {vars} defs opts = eval {vars} defs opts

evalClosure defs (MkClosure opts locs env tm)
    = eval defs opts env locs tm []
evalClosure defs (MkNFClosure opts env nf)
    = applyToStack defs opts env True nf []

export
evalClosureWithOpts : {auto c : Ref Ctxt Defs} ->
                      {free : _} ->
                      Defs -> EvalOpts -> Closure free -> Core (NF free)
evalClosureWithOpts defs opts (MkClosure _ locs env tm)
    = eval defs opts env locs tm []
evalClosureWithOpts defs opts (MkNFClosure _ env nf)
    = applyToStack defs opts env True nf []

export
nf : {auto c : Ref Ctxt Defs} ->
     {vars : _} ->
     Defs -> Env Term vars -> Term vars -> Core (NF vars)
nf defs env tm = eval defs defaultOpts env [] tm []

export
nfOpts : {auto c : Ref Ctxt Defs} ->
         {vars : _} ->
         EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)
nfOpts opts defs env tm = eval defs opts env [] tm []

export
gnf : {vars : _} ->
      Env Term vars -> Term vars -> Glued vars
gnf env tm
    = MkGlue True
             (pure tm)
             (\c => do defs <- get Ctxt
                       nf defs env tm)

export
gnfOpts : {vars : _} ->
          EvalOpts -> Env Term vars -> Term vars -> Glued vars
gnfOpts opts env tm
    = MkGlue True
             (pure tm)
             (\c => do defs <- get Ctxt
                       nfOpts opts defs env tm)

export
gType : FC -> Glued vars
gType fc = MkGlue True (pure (TType fc)) (const (pure (NType fc)))

export
gErased : FC -> Glued vars
gErased fc = MkGlue True (pure (Erased fc False)) (const (pure (NErased fc False)))

-- Resume a previously blocked normalisation with a new environment
export
continueNF : {auto c : Ref Ctxt Defs} ->
             {vars : _} ->
             Defs -> Env Term vars -> NF vars -> Core (NF vars)
continueNF defs env stuck
   = applyToStack defs defaultOpts env True stuck []


text:
module Control.Monad.Spawn

%default total

public export
interface Monad m => CanSpawn m where
  spawn : m Unit -> m Unit


text:
module Military

public export
record Military where
  constructor CreateMilitary
  unit : String
  unitID : Integer
  countryID : Integer
  from : Integer
  until : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Flutter.Widgets.Functions

import Dart.FFI
import Flutter.FFI
import public Dart.Core
import public Dart.FFI.Upcast

%inline
export
runApp : {widget : Type} -> IsAssignableFrom Widget widget => widget -> IO ()
runApp w = primIO (prim__dart_invoke "runApp,package:flutter/widgets.dart" [] [w] none)

||| A simpler alternative to `pure (cast widget)`.
%inline
export
widget : {a : Type} -> Cast a Widget => a -> IO Widget
widget w = pure (cast w)

%inline
export
widgets : UpcastList Widget -> Core.List Widget
widgets = fromList . toList


text:
-- Idris2

import System
import System.Concurrency

||| Test releasing without acquiring errors correctly
main : IO ()
main =
  do m <- makeMutex
     mutexRelease m
     putStrLn "Released w/o acquiring (SHOULDN'T HAPPEN)"


text:
data Test : Type where
     MkTest : Integer -> Integer -> Test

etaGood1 : MkTest = (\x => \y => MkTest ? ?)
etaGood1 = Refl

etaGood2: (MkTest 1) = (\x => MkTest ? x)
etaGood2 = Refl

etaGood3: (f : a -> b) -> f = (\x => f x)
etaGood3 f = Refl

etaBad : MkTest = (\x : Nat => \y => MkTest ? ?)
etaBad = Refl


text:
import Language.Reflection

x : TTImp
x = `(with Prelude.Nil [])

%language ElabReflection

x' : Elab (List Nat)
x' = check x

l : List Nat
l = 1 :: %runElab x'

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Effect.State

import Effects

%access public

data State : Effect where
  Get :      { a }       State a
  Put : b -> { a ==> b } State ()

using (m : Type -> Type)
  instance Handler State m where
     handle st Get     k = k st st
     handle st (Put n) k = k () n

STATE : Type -> EFFECT
STATE t = MkEff t State

get : { [STATE x] } Eff m x
get = Get

put : x -> { [STATE x] } Eff m ()
put val = Put val

putM : y -> { [STATE x] ==> [STATE y] } Eff m ()
putM val = Put val

update : (x -> x) -> { [STATE x] } Eff m ()
update f = put (f !get)

updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff m ()
updateM f = putM (f !get)

locally : x -> ({ [STATE x] } Eff m t) -> { [STATE y] } Eff m t
locally newst prog = do st <- get
                        putM newst
                        val <- prog
                        putM st
                        return val

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
module PQ.Schema

import Control.Monad.Either

import Data.List
import Data.String
import Data.SOP

import PQ.FFI
import PQ.Types

%default total

--------------------------------------------------------------------------------
--          Data Types
--------------------------------------------------------------------------------

public export
data PQPrim : Type where
  SmallInt        : PQPrim
  PQInteger       : PQPrim
  BigInt          : PQPrim
  DoublePrecision : PQPrim
  Text            : PQPrim
  VarChar         : Bits32 -> PQPrim
  Boolean         : PQPrim

export
primSchema : PQPrim -> String
primSchema SmallInt        = "smallint"
primSchema PQInteger       = "integer"
primSchema BigInt          = "bigint"
primSchema DoublePrecision = "double precision"
primSchema Text            = "text"
primSchema (VarChar n)     = #"varchar(\#{show n})"#
primSchema Boolean         = "boolean"

public export
PrimType : PQPrim -> Type
PrimType SmallInt        = Int16
PrimType PQInteger       = Int32
PrimType BigInt          = Int64
PrimType DoublePrecision = Double
PrimType Text            = String
PrimType (VarChar _)     = String
PrimType Boolean         = Bool

export
encodePrimType : (tpe : PQPrim) -> PrimType tpe -> String
encodePrimType SmallInt x        = show x
encodePrimType PQInteger x       = show x
encodePrimType BigInt x          = show x
encodePrimType DoublePrecision x = show x
encodePrimType Text x            = #"'\#{x}'"#
encodePrimType (VarChar _) x     = #"'\#{x}'"#
encodePrimType Boolean True      = "TRUE"
encodePrimType Boolean False     = "FALSE"

export
decodePrimType : (tpe : PQPrim) -> String -> PrimType tpe
decodePrimType SmallInt x        = cast x
decodePrimType PQInteger x       = cast x
decodePrimType BigInt x          = cast x
decodePrimType DoublePrecision x = cast x
decodePrimType Text x            = x
decodePrimType (VarChar _) x     = x
decodePrimType Boolean "t"       = True
decodePrimType Boolean _         = False

public export
data PQType : Type where
  NotNull  : PQPrim -> PQType
  Nullable : PQPrim -> PQType

public export
DBType : PQType -> Type
DBType (NotNull p)  = PrimType p
DBType (Nullable p) = Maybe $ PrimType p

export
encodeDBType : (tpe : PQType) -> DBType tpe -> String
encodeDBType (NotNull p)  v        = encodePrimType p v
encodeDBType (Nullable p) (Just v) = encodePrimType p v
encodeDBType (Nullable p) Nothing  = "DEFAULT"

export
decodeDBType : (tpe : PQType) -> String -> DBType tpe
decodeDBType (NotNull p)  s  = decodePrimType p s
decodeDBType (Nullable p) "" = Nothing
decodeDBType (Nullable p) s  = Just $ decodePrimType p s

--------------------------------------------------------------------------------
--          Table Columns
--------------------------------------------------------------------------------

public export
data Default : PQType -> Type where
  Null        : {0 any : PQPrim} -> Default (Nullable any)
  NoDefault   : {0 any : PQPrim} -> Default (NotNull any)
  Value       : {0 any : PQPrim} -> PrimType any -> Default (NotNull any)
  SmallSerial : Default (NotNull SmallInt)
  Serial      : Default (NotNull PQInteger)
  BigSerial   : Default (NotNull BigInt)

defaultSchema : {tpe : _} -> Default tpe -> String
defaultSchema SmallSerial = "SMALLSERIAL"
defaultSchema Serial      = "SERIAL"
defaultSchema BigSerial   = "BIGSERIAL"
defaultSchema {tpe = Nullable p} Null      = primSchema p
defaultSchema {tpe = NotNull p}  NoDefault = #"\#{primSchema p} NOT NULL"#
defaultSchema {tpe = NotNull p} (Value v)  =
  #"\#{primSchema p} DEFAULT \#{encodePrimType p v}"#

public export
data Constraint : Type where
  Vanilla      : Constraint
  PrimaryKey   : Constraint
  Unique       : Constraint

constraintSchema : Constraint -> String
constraintSchema Vanilla    = ""
constraintSchema PrimaryKey = " PRIMARY KEY"
constraintSchema Unique     = " UNIQUE"

public export
PutType : Default t -> Type -> Type
PutType Null        t = t
PutType NoDefault   t = t
PutType (Value x)   t = Maybe t
PutType SmallSerial _ = ()
PutType Serial      _ = ()
PutType BigSerial   _ = ()

public export
record Column where
  constructor MkField
  0 idrisTpe : Type
  name       : String
  pqType     : PQType
  constraint : Constraint
  deflt      : Default pqType
  fromPQ     : DBType pqType -> Maybe idrisType
  toPQ       : PutType deflt idrisTpe -> PutType deflt (DBType pqType)
  table_name : String

export
encodePutType :  {tpe : _}
              -> (deflt : Default tpe)
              -> PutType deflt (DBType tpe)
              -> String
encodePutType Null x             = encodeDBType tpe x
encodePutType NoDefault x        = encodeDBType tpe x
encodePutType (Value y) (Just x) = encodeDBType tpe x
encodePutType (Value y) Nothing  = "DEFAULT"
encodePutType SmallSerial x      = "DEFAULT"
encodePutType Serial x           = "DEFAULT"
encodePutType BigSerial x        = "DEFAULT"

public export
0 PutTypeC : Column -> Type
PutTypeC (MkField idrisTpe _ _ _ def _ _ _) = PutType def idrisTpe

public export
0 GetTypeC : Column -> Type
GetTypeC c = c.idrisType

public export
primarySerial16 : (0 t : Type) -> String -> (Int16 -> Maybe t) -> String -> Column
primarySerial16 t n f tn =
  MkField t n (NotNull SmallInt) PrimaryKey SmallSerial f id tn

public export
primarySerial32 : (0 t : Type) -> String -> (Int32 -> Maybe t) -> String -> Column
primarySerial32 t n f tn=
  MkField t n (NotNull PQInteger) PrimaryKey Serial f id tn

public export
primarySerial64 : (0 t : Type) -> String -> (Int64 -> Maybe t) -> String -> Column
primarySerial64 t n f tn=
  MkField t n (NotNull BigInt) PrimaryKey BigSerial f id tn

public export
notNull : (0 t : Type)
        -> String
        -> (pq : PQPrim)
        -> (decode : PrimType pq -> Maybe t)
        -> (encode : t -> PrimType pq)
        -> (tn: String)
        -> Column
notNull t n pq dec enc tn=
  MkField t n (NotNull pq) Vanilla NoDefault dec enc tn

public export
notNullDefault : (0 t : Type)
               -> String
               -> (pq   : PQPrim)
               -> (dflt : PrimType pq)
               -> (decode : PrimType pq -> Maybe t)
               -> (encode : t -> PrimType pq)
               -> String
               -> Column
notNullDefault t n pq dflt dec enc tn=
  MkField t n (NotNull pq) Vanilla (Value dflt) dec (map enc) tn

public export
nullable : (0 t : Type)
         -> String
         -> (pq : PQPrim)
         -> (decode : PrimType pq -> Maybe t)
         -> (encode : t -> PrimType pq)
         -> (tn: String)
         -> Column
nullable t n pq dec enc tn =
  MkField (Maybe t) n (Nullable pq) Vanilla Null (maybe (Just Nothing) (map Just . dec)) (map enc) tn

export
columnSchema : Column -> String
columnSchema (MkField _ name tpe con dflt _ _ _) =
  #"\#{name} \#{defaultSchema dflt}\#{constraintSchema con}"#

--------------------------------------------------------------------------------
--          Table
--------------------------------------------------------------------------------

public export
record Table where
  constructor MkTable
  name    : String
  columns : List Column

export
createTableSQL : Table -> String
createTableSQL (MkTable name columns) =
  let cols = fastConcat $ intersperse ",\n" $ map (("  " ++) . columnSchema) columns
   in #"""
      CREATE TABLE \#{name} (
      \#{cols}
      );
      """#

export
createTable : HasIO io => MonadError SQLError io => Connection -> Table -> io ()
createTable c t = exec_ c (createTableSQL t) COMMAND_OK

--------------------------------------------------------------------------------
--          Queries
--------------------------------------------------------------------------------

public export
data EqPrim : PQPrim -> Type where
  EqSmallInt        : EqPrim SmallInt
  EqPQInteger       : EqPrim PQInteger
  EqBigInt          : EqPrim BigInt
  EqDoublePrecision : EqPrim DoublePrecision
  EqText            : EqPrim Text
  EqBoolean         : EqPrim Boolean

public export
data Eq : PQType -> Type where
  EqNotNull  : EqPrim p -> Eq (NotNull p)
  EqNullable : EqPrim p -> Eq (Nullable p)

public export
data OrdPrim : PQPrim -> Type where
  OrdSmallInt        : OrdPrim SmallInt
  OrdPQInteger       : OrdPrim PQInteger
  OrdBigInt          : OrdPrim BigInt
  OrdDoublePrecision : OrdPrim DoublePrecision
  OrdText            : OrdPrim Text
  OrdBoolean         : OrdPrim Boolean

public export
data Ord : PQType -> Type where
  OrdNotNull  : OrdPrim p -> Ord (NotNull p)
  OrdNullable : OrdPrim p -> Ord (Nullable p)

public export
data IsNullable : PQType -> Type where
  ItIsNullable : {0 p : PQPrim} -> IsNullable (Nullable p)

public export
data Op : Type where
  JC : (c1 : Column) -> (c2 : Column) -> Op
  (==)  : (c : Column) -> DBType (pqType c) -> {auto 0 _ : Eq (pqType c)} -> Op
  (/=)  : (c : Column) -> DBType (pqType c) -> {auto 0 _ : Eq (pqType c)} -> Op
  (>)   : (c : Column) -> DBType (pqType c) -> {auto 0 _ : Ord (pqType c)} -> Op
  (>=)  : (c : Column) -> DBType (pqType c) -> {auto 0 _ : Ord (pqType c)} -> Op
  (<)   : (c : Column) -> DBType (pqType c) -> {auto 0 _ : Ord (pqType c)} -> Op
  (<=)  : (c : Column) -> DBType (pqType c) -> {auto 0 _ : Ord (pqType c)} -> Op
  IsNull    : (c : Column) -> {auto 0 _ : IsNullable (pqType c)} -> Op
  IsNotNull : (c : Column) -> {auto 0 _ : IsNullable (pqType c)} -> Op
  (&&)  : Op -> Op -> Op
  (||)  : Op -> Op -> Op
  Not   : Op -> Op
  True  : Op
  False : Op

export
opToSQL : Op -> String
opToSQL (JC c1 c2)  = #"\#{c1.table_name}.\#{c1.name}=\#{c2.table_name}.\#{c2.name}"#
opToSQL (c == x)      = #"\#{c.name} = \#{encodeDBType c.pqType x}"#
opToSQL (c /= x)      = #"\#{c.name} <> \#{encodeDBType c.pqType x}"#
opToSQL (c > x)       = #"\#{c.name} > \#{encodeDBType c.pqType x}"#
opToSQL (c >= x)      = #"\#{c.name} >= \#{encodeDBType c.pqType x}"#
opToSQL (c < x)       = #"\#{c.name} < \#{encodeDBType c.pqType x}"#
opToSQL (c <= x)      = #"\#{c.name} <= \#{encodeDBType c.pqType x}"#
opToSQL (IsNull c)    = #"\#{c.name} IS NULL"#
opToSQL (IsNotNull c) = #"\#{c.name} IS NOT NULL"#
opToSQL (x && y)      = #"(\#{opToSQL x}) AND (\#{opToSQL y})"#
opToSQL (Not x)       = #"NOT (\#{opToSQL x})"#
opToSQL (x || y)      = #"(\#{opToSQL x}) OR (\#{opToSQL y})"#
opToSQL True          = "TRUE"
opToSQL False         = "FALSE"


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Run

import Options.Applicative.Types
import Options.Applicative.Maybe
import Control.Monad.State
import Control.Monad.Trans

%default total
%access public export

record OptWord where
  constructor ParsedWord
  name : OptName
  wordVal : Maybe String

parseWord : String -> Maybe OptWord
parseWord s = case unpack s of
  ('-' :: '-' :: w) => Just $ case span (/= '=') w of
        (_, [])         => ParsedWord (LongName . pack $ w) Nothing
        (w', _ :: rest) => ParsedWord (LongName . pack $ w') $ Just . pack $ rest
  ('-' :: w :: [])  => Just $ ParsedWord (ShortName w) Nothing
  ('-' :: w :: rs)  => Just $ ParsedWord (ShortName w) $ Just (pack rs)
  _                 => Nothing

searchParser : {a : Type} -> Parser a
           -> ({g : ParamType} -> {r : Type} -> Option g r -> MaybeT (StateT (List String) (Either ParseError)) (Parser r))
           -> MaybeT (StateT (List String) (Either ParseError)) (Parser a)
searchParser (NilP x)     _ = empty
searchParser (OptP o)     f = f o
searchParser (AppP p1 p2) f =
  ((\p1' => p1' <*> p2) <$> searchParser p1 f)
  <|>
  ((\p2' => p1 <*> p2') <$> searchParser p2 f)
searchParser (AltP p1 p2) f = searchParser p1 f <|> searchParser p2 f

stepParser : {a : Type} -> Parser a -> String -> MaybeT (StateT (List String) (Either ParseError)) (Parser a)
stepParser p arg = case parseWord arg of
  Nothing => searchParser p $ \opt => case opt of
    Opt _ (ArgReader fa _) => lift $ lift $ map pure (fa arg)
    Opt _ (CmdReader ps _) => case lookup arg ps of
      Just sub => pure sub
      Nothing  => empty
    _                      => empty
  Just (ParsedWord w wordVal) => searchParser p $ \opt => case opt of
    Opt _ (FlagReader w' a)    => case elem w w' of
      True  => do
        args <- lift $ ST $ \x => pure (x, x)
        let poppedArgs  = maybe [] (\w => ("-" <+> w) :: Nil) wordVal <+> args
        lift $ ST (\y => pure ((), poppedArgs))
        lift . lift . Right . pure $ a
      False => empty
    Opt _ (OptionReader w' fa _) => case elem w w' of
      True  => do
        args <- lift $ ST $ \x => pure (x, x)
        let argsWord = maybe [] (:: Nil) wordVal <+> args
        case argsWord of
          (a :: rest) => do
            lift $ ST $ \y => pure ((), rest)
            lift . lift . map pure $ fa a
          _ => lift $ lift (Left $ ErrorMsg "Input required after option ")
      False => empty
    _ => empty

evalParser : Parser a -> Maybe a
evalParser (NilP r)     = r
evalParser (OptP _)     = Nothing
evalParser (AppP p1 p2) = evalParser p1 <*> evalParser p2
evalParser (AltP p1 p2) = evalParser p1 <|> evalParser p2

parseError : String -> ParseError
parseError arg = ErrorMsg $ case unpack arg of
  ('-'::_) => "Invalid option `" ++ arg ++ "'"
  _        => "Invalid argument `" ++ arg ++ "'"

total
runParser : Parser a -> List String -> Either ParseError (a, List String)
runParser p Nil = maybeToEither (ErrorMsg "Not enough input") $ map (\p' => (p', Nil)) (evalParser p)
runParser p args@(arg :: argt) = do
  (Just p', args') <- runStateT (runMaybeT $ stepParser p arg) argt
    | _ => maybeToEither (parseError arg) (map (\x' => (x', args)) (evalParser p))
  assert_total $ runParser p' args'

total
runParserFully : Parser a -> List String -> Either ParseError a
runParserFully p ls = do
  (res,leftOver) <- runParser p ls
  case leftOver of
    (un :: _) => Left $ parseError un
    Nil       => Right res

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris


text:
module PermConsProperties

import Data.Vect
import congruence
import PermCons

%access public export
%default total

||| a :: (perm xs) = (includePerm perm) (a :: xs)

PermC_prp_1 : (n : Nat) -> (a : Nat) -> (xs : (Vect n Nat)) ->
              (perm : (PermC n)) ->
              ( (a :: (applyPerm n Nat perm xs)) =
                (applyPerm (S n) Nat (includePerm n perm) (a :: xs)))

PermC_prp_1 Z a Nil perm = Refl
PermC_prp_1 (S Z) a [x] perm = Refl
PermC_prp_1 (S (S k)) a xs (Idt (S (S k))) = Refl
PermC_prp_1 (S (S k)) a xs (Swap (S (S k)) FZ) = Refl
PermC_prp_1 (S (S k)) a xs (Swap (S (S k)) (FS l)) = Refl
PermC_prp_1 (S (S k)) a xs (CPerm (S (S k)) f g) = let

    f1 = applyPerm (S (S k)) Nat f
    f2 = applyPerm (S (S (S k))) Nat (includePerm (S (S k)) f)
    g1 = applyPerm (S (S k)) Nat g
    g2 = applyPerm (S (S (S k))) Nat (includePerm (S (S k)) g)

    pf1 = PermC_prp_1 (S (S k)) a xs g -- a :: (g1 xs) = (includePerm g1) (a :: xs)
    pf2 = congruence (Vect (S (S (S k))) Nat) (Vect (S (S (S k))) Nat)
        (a :: (g1 xs)) (g2 (a :: xs)) f2 pf1 -- f2 (a :: g1 xs) = f2 (g2 (a :: xs))

    v1 = g1 xs

    pf3 = PermC_prp_1 (S (S k)) a v1 f -- a :: (f1 v1) = f2 (a :: v1)
    in
    (trans pf3 pf2)

PermC_prp_2 : (n : Nat) -> (u : (Vect n Nat)) -> ((applyPerm n Nat (Idt n) u) = u)
PermC_prp_2 Z u = Refl
PermC_prp_2 (S Z) u = Refl
PermC_prp_2 (S (S k)) u = Refl


text:
{-
0
1
2
-}
module Main

length' : List a -> Nat
length' = length'' Z
  where length'' acc []      = acc
        length'' acc (x::xs) = length'' (S acc) xs

printList : List String -> IO ()
printList (x :: xs) = do putStrLn x
                         printList xs
printList []        = return ()

main : IO ()
main = do printList $ map (show . length') lists
--          printList $ map show $ sort [3, 4, 1]
  where lists : List (List Nat)
        lists = [[1..l] | l <- [0..2]]

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Scheme.Core

import Control.Isomorphism
import Data.Vect

%default total
%access public export

-- TODO Integer <= Rational <= Real <= Complex
-- TODO Exact | Inexact
||| [S]cheme [Num]ber
data SNum : Type where
  SNExactInt : Integer -> SNum

||| [S]ymbolic [Exp]ression
data SExp : Type where
  ||| Symbols are just identifiers or pointers
  ||| They evaluate to something if defined in current scope
  ||| Some are special forms that are evaluated under different rules
  SESymbol  : String -> SExp
  ||| Unit is an empty list
  SEUnit    : SExp
  ||| Cons is the basic building block and the only way to apply a function
  SECons    : SExp -> SExp -> SExp
  ||| Vector should be just an O(1) access List
  ||| Vectors are terminal
  SEVect    : Vect n SExp -> SExp
  ||| Booleans are terminal
  SEBool    : Bool -> SExp
  ||| Chars are terminal
  SEChar    : Char -> SExp
  ||| Strings are terminal
  SEStr     : String -> SExp
  ||| Numbers are terminal
  SENum     : SNum -> SExp

listify : SExp -> (List SExp, Maybe SExp)
listify SEUnit       = ([], Nothing)
listify (SECons x y) = let (ls, md) = listify y
                        in (x :: ls, md)
listify x            = ([], Just x)

unListify : (List SExp, Maybe SExp) -> SExp
unListify (xs, ms) = foldr SECons (maybe SEUnit id ms) xs

-- unListify : (List SExp, Maybe SExp) -> SExp
-- unListify ([]     , Nothing) = SEUnit
-- unListify ([]     , Just s ) = s
-- unListify (x :: xs, ms     ) = SECons x $ assert_total $ unListify (xs, ms)

-- ||| A theorem about lists and dotted lists
-- lispIso : Iso SExp (List SExp, Maybe SExp)
-- lispIso = MkIso to from toFrom fromTo
--   where
--     to : SExp -> (List SExp, Maybe SExp)
--     to = listify
--     from : (List SExp, Maybe SExp) -> SExp
--     from = unListify
--     toFrom : (p : (List SExp, Maybe SExp)) -> to (from p) = p
--     toFrom ([]     , Nothing) = Refl
--     toFrom ([]     , Just s ) = ?toFrom_rhs_5
--     toFrom (x :: xs, Nothing) = ?toFrom_rhs_4
--     toFrom (x :: xs, Just s ) = ?toFrom_rhs_1
--     fromTo : (s : SExp) -> from (to s) = s
--     fromTo SEUnit       = Refl
--     fromTo (SESymbol x) = Refl
--     fromTo (SEVect xs ) = Refl
--     fromTo (SEBool x  ) = Refl
--     fromTo (SEChar x  ) = Refl
--     fromTo (SEStr x   ) = Refl
--     fromTo (SENum x   ) = Refl
--     fromTo (SECons x y) = ?whasdasd


text:
module Resugar

niceList : List (Nat, Nat)
niceList = [ (i, j) | i <- [0..4], j <- [5..9] ]


text:
module Circuits.Idealised.Main

import System
import System.File

import Data.String
import Data.List1

import Text.Lexer
import Text.Parser

import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Run

import Toolkit.Data.List.Occurs.Does
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree

import Circuits.Idealised.Types
import Circuits.Idealised.Terms
import Circuits.Idealised.AST
import Circuits.Idealised.Lexer
import Circuits.Idealised.Parser
import Circuits.Idealised.Check
import Circuits.Idealised.Interp

export
Show a => Show (ParseFailure a) where
  show err
    = trim $ unlines [show (location err), (error err)]

export
Show a => Show (ParseError a) where
  show (FError err)
    = trim $ unlines ["File Error: "
                     , show err]
  show (PError err)
    = trim $ unlines (forget (map show err))

  show (LError (MkLexFail l i))
    = trim $ unlines [show l, show i]

export
Show (Vertex String) where
  show (Node d k j i) = show k <+> " [label=\"" <+> show (j,i) <+> " " <+> d <+> "\"];"
  show (Leaf d x k j) = show k <+> " [label=\"" <+> withFlow x j <+> " " <+> d <+> "\"];"
    where withFlow : Flow -> Nat -> String
          withFlow f k = show f <+> "(" <+> show k <+>")"

export
showGraph : Graph String -> String
showGraph (MkGraph nodes edges)
    = unlines $ ["digraph G {"]
                ++
                  map show nodes
                ++
                  map (\(x,y) => unwords ["\t" <+> show x, "->", show y <+> ";"]) edges
                ++
                ["}"]

export
Show DegreeType where
  show I = "IN"
  show O = "OUT"

export
showErr : (Graph String, HasExactDegree.Error String)  -> String
showErr (g, MkError vertex kind (MkError vertexID k values))
 = unlines [showGraph g
           , "//because:"
           , "// Vertex " <+> show (ident vertex)
           , "//  has expected degree " <+> show k <+> " " <+> show (values.expected)
           , "//  but we found degree " <+> show k <+> " " <+> show (values.found)
           ]

main : IO Unit
main
  = do putStrLn "// LOG : Starting Idealised Linear "
       args <- getArgs

       case args of
         [x,y] => do Right ast <- fromFile y
                       | Left err => do putStrLn "// LOG : Failure Parsing"
                                        printLn err
                                        exitFailure
                     Right term <- typeCheckIO ast
                        | Left err => do putStrLn "// LOG : Failure Type Checking"
                                         printLn err
                                         exitFailure
                     Right res <- runIO term
                        | Left err => do putStrLn "// LOG : Failure Interpreting"
                                         putStrLn (showErr err)
                                         exitFailure
                     putStrLn ((showGraph . fst . getGraph) res)
                     exitSuccess
         _ => do putStrLn "need at least a file name"
                 exitFailure

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Text.WebIDL.Types.Err

import Text.WebIDL.Types.Token
import Text.Lexer
import Generics.Derive

%default total

%language ElabReflection

||| Errors that can happen during lexing and parsing.
public export
data Err : Type where
  ||| An error that happened during lexing
  LexErr     : (msg : String) -> Err

  ||| The parser will fail with this error, if not all tokens
  ||| have been consumed at the end of parsing.
  ||| The error constains position and content of the next token.
  NoEOI      : (tok : WithBounds IdlToken) -> Err

  ||| There was an error in the parser but all tokens were already
  ||| consumed.
  ParseErr   :  (msg : String) -> Err

  ||| There was an error in the parser and the position
  ||| is given.
  ParseErrAt :  (msg : String)
             -> (line : Int)
             -> (col : Int)
             -> Err

%runElab derive "Err" [Generic,Meta,Eq,Show]


text:
module System.Path

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

import System.Info

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

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 prefixes of path component.
public export
data Volume
  =
  ||| Windows' Uniform Naming Convention, e.g., a network sharing
  ||| directory: `\\host\c$\Windows\System32`
  UNC String String |
  ||| The drive, e.g., "C:". The disk character is in upper case
  Disk Char

||| A single body of path component.
public export
data Body
  =
  ||| Represents "."
  CurDir |
  ||| Represents ".."
  ParentDir |
  ||| Common directory or file
  Normal String

||| A parsed cross-platform file system path.
|||
||| The function `parse` constructs a Path component from String,
||| and the function `show` converts in reverse.
|||
||| Trailing separator is only used for display and is ignored while
||| comparing paths.
public export
record Path where
    constructor MkPath
    ||| Windows' path prefix (only on Windows)
    volume : Maybe Volume
    ||| Whether the path contains a 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 that represents "".
public export
emptyPath : Path
emptyPath = MkPath Nothing False [] False

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

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

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

||| Display the path in the format on the platform.
export
Show Path where
  show p = let sep = singleton dirSeparator
               volStr = fromMaybe "" (map show p.volume)
               rootStr = if p.hasRoot then sep else ""
               bodyStr = join sep $ map show p.body
               trailStr = if p.hasTrailSep then sep else "" in
             volStr ++ rootStr ++ bodyStr ++ trailStr

--------------------------------------------------------------------------------
-- 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 PathToken
lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in
                map TokenData.tok tokens

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

-- Example: \\?\
-- Windows can automatically translate '/' to '\\'. The verbatim prefix,
-- i.e., `\\?\`, disables the translation.
-- Here, we simply parse and then ignore it.
verbatim : Grammar PathToken True ()
verbatim = do count (exactly 2) $ match $ PTPunct '\\'
              match $ PTPunct '?'
              match $ PTPunct '\\'
              pure ()

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

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

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

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

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

parseBody : Grammar PathToken True Body
parseBody = do text <- match PTText
               the (Grammar _ False _) $
                   case text of
                        ".." => pure ParentDir
                        "." => pure CurDir
                        s => pure (Normal s)

parsePath : Grammar 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)

||| Parse a String into Path component.
|||
||| Returns the path parsed as much as possible from left to right, the
||| invalid parts on the right end is ignored.
|||
||| Some kind of invalid path is accepted. Relaxing rules:
|||
||| - Both slash('/') and backslash('\\') are parsed as valid directory
|||   separator, regardless of the platform;
||| - Any characters in path body in allowed, e.g., glob like "/root/*";
||| - Verbatim prefix(`\\?\`) that disables the forward
|||   slash (Windows only) is ignored.
||| - Repeated separators are ignored, so "a/b" and "a//b" both have "a"
|||   and "b" as bodies.
||| - Occurrences of "." are normalized away, except if they are at the
|||   beginning of the path. For example, "a/./b", "a/b/", "a/b/". and
|||   "a/b" all have "a" and "b" as bodies, but "./a/b" starts with an
|||   additional `CurDir` body.
|||
||| ```idris example
||| parse "C:\\Windows/System32"
||| ```
||| ```idris example
||| parse "/usr/local/etc/*"
||| ```
export
parse : String -> Path
parse str = case parse parsePath (lexPath str) of
                 Right (p, _) => p
                 _ => emptyPath

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

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

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

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

parent' : Path -> Maybe Path
parent' p = map fst (splitParent' p)

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

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

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

--------------------------------------------------------------------------------
-- Manipulations
--------------------------------------------------------------------------------

||| 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 has a volume and starts
|||   with the root. e.g., `c:\\windows` is absolute, while `c:temp`
|||   and `\temp` are not. In addition, a path with UNC volume is absolute.
export
isAbsolute : String -> Bool
isAbsolute p = isAbsolute' (parse p)

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

||| Appends the right path to the left one.
|||
||| 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"
||| ```
export
(</>) : (left : String) -> (right : String) -> String
(</>) l r = show $ append' (parse l) (parse r)

||| Join path elements together.
|||
||| ```idris example
||| joinPath ["/usr", "local/etc"] == "/usr/local/etc"
||| ```
export
joinPath : List String -> String
joinPath xs = foldl (</>) "" xs

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

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

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

||| Determines whether base is either one of the parents of full.
|||
||| Trailing separator is ignored.
export
startWith : (base : String) -> (full : String) -> Bool
startWith base full = (parse base) `elem` (iterate parent' (parse full))

||| Returns a path that, when appended onto base, yields full.
|||
||| If base is not a prefix of full (i.e., startWith returns false),
||| returns Nothing.
export
stripPrefix : (base : String) -> (full : String) -> Maybe String
stripPrefix base full
    = do let MkPath vol1 root1 body1 _ = parse base
         let MkPath vol2 root2 body2 trialSep = parse full
         if vol1 == vol2 && root1 == root2 then Just () else Nothing
         body <- stripBody body1 body2
         pure $ show $ MkPath Nothing False body trialSep
  where
    stripBody : (base : List Body) -> (full : List Body) -> Maybe (List Body)
    stripBody [] ys = Just ys
    stripBody xs [] = Nothing
    stripBody (x::xs) (y::ys) = if x == y then stripBody xs ys else Nothing

||| Returns the final body of the path, if there is one.
|||
||| If the path is a normal file, this is the file name. If it's the
||| path of a directory, this is the directory name.
|||
||| Returns Nothing if the final body is "..".
export
fileName : String -> Maybe String
fileName p = fileName' (parse p)

||| Extracts the stem (non-extension) portion of the file name of path.
|||
||| 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 "." and has
|||   no other "."s within;
||| - Otherwise, the portion of the file name before the final "."
export
fileStem : String -> Maybe String
fileStem p = pure $ fst $ splitFileName !(fileName p)

||| Extracts the extension of the file name of path.
|||
||| The extension is:
|||
||| - Nothing, if there is no file name;
||| - Nothing, if there is no embedded ".";
||| - Nothing, if the file name begins with "." and has no other "."s within;
||| - Otherwise, the portion of the file name after the final "."
export
extension : String -> Maybe String
extension p = pure $ snd $ splitFileName !(fileName p)

||| Updates the file name of the path.
|||
||| If no file name, this is equivalent to appending the name;
||| Otherwise it is equivalent to appending the name to the parent.
export
setFileName : (name : String) -> String -> String
setFileName name p = show $ setFileName' name (parse p)

||| Append a extension to the path.
|||
||| Returns the path as it is if no file name.
|||
||| If `extension` of the path is Nothing, the extension is added; otherwise
||| it is replaced.
|||
||| If the ext is empty, the extension is dropped.
export
(<.>) : String -> (ext : String) -> String
(<.>) p ext = let p' = parse p
                  ext = pack $ dropWhile (== '.') (unpack ext)
                  ext = if ltrim ext == "" then "" else "." ++ ext in
                case fileName' p' of
                     Just name => let (stem, _) = splitFileName name in
                                    show $ setFileName' (stem ++ ext) p'
                     Nothing => p