text:
module Depling.Unification

import Depling
import Depling.Pull
import Depling.Reduce
import Utils
import Data.Fin
import Data.Vect

public export
data UnificationGroup : Nat -> Nat -> Type where
	UnificationGroupV : (es : List (Either (DAST l) (DAST r))) -> {auto ne : NonEmpty es} -> UnificationGroup l r

total
export
map : (Either (DAST l1) (DAST r1) -> Either (DAST l2) (DAST r2)) -> UnificationGroup l1 r1 -> UnificationGroup l2 r2
map f (UnificationGroupV es {ne}) = UnificationGroupV (map f es) {ne = nonEmptyMap ne}

total
find : Either (DAST l) (DAST r) -> List (UnificationGroup l r) -> (Maybe (UnificationGroup l r), List (UnificationGroup l r))
find e [] = (Nothing, [])
find e (g@(UnificationGroupV es) :: us) =
	if elem e es
	then (Just g, us)
	else
		let (g', us') = find e us
		in (g', g :: us')

total
is_concrete : DAST n -> Bool
is_concrete (ʌ _) = False
is_concrete _ = True

mutual
  total
  export
  is_similar : DAST l -> DAST r -> Bool
  is_similar l r = assert_total $ is_similar' (lfreduce l) (lfreduce r)

  total
  is_similar' : DAST l -> DAST r -> Bool
  is_similar' (ʌ _) _ = True
  is_similar' _ (ʌ _) = True
  is_similar' 𝕋 𝕋 = True
  is_similar' (𝕌 ln lt) (𝕌 rn rt) = ln == rn && is_similar lt rt
  is_similar' (ℂ {a=la} lc las) (ℂ {a=ra} rc ras) =
    la == ra &&
    lc == believe_me rc &&
    (assert_total $ and $ zipWith (\a, b => assert_total $ is_similar a b) (toList las) (toList ras))
  is_similar' (𝔹 lt) (𝔹 rt) = is_similar lt rt
  is_similar' l r = False

total
pull_group : UnificationGroup (S l) (S r) -> Maybe (UnificationGroup l r)
pull_group {l} {r} (UnificationGroupV es) =
	case
		catMaybes $
		map (either (map Left . pull 0) (map Right . pull 0)) es
	of
		[] => Nothing
		es@(_ :: _) => Just $ UnificationGroupV es

total
pull_group' : UnificationGroup (a + l) (a + r) -> Maybe (UnificationGroup l r)
pull_group' {a=Z} g = Just g
pull_group' {a=S a} g = pull_group g >>= pull_group'

mutual
	do_merge : UnificationGroup l r -> (UnificationGroup l r, List (UnificationGroup l r)) -> (UnificationGroup l r, List (UnificationGroup l r))
	do_merge (UnificationGroupV g1) (g2, us) = assert_total $ foldr add_to_group (g2, us) g1

	total
	try_merge1 : UnificationGroup l r -> UnificationGroup l r -> Maybe (UnificationGroup l r, List (UnificationGroup l r))
	try_merge1 g1@(UnificationGroupV es1) g2@(UnificationGroupV es2) =
		if or $ map (\e => elem e es2) es1
		then Just $ do_merge g1 (g2, [])
		else Nothing

	total
	merge : UnificationGroup l r -> List (UnificationGroup l r) -> List (UnificationGroup l r) -> List (UnificationGroup l r)
	merge g [] us' = g :: us'
	merge g (g' :: us) us' =
		case try_merge1 g g' of
			Just (g', us'') => g' :: assert_total (mergeMany us'' (us ++ us'))
			Nothing => merge g us (g' :: us')

	total
	mergeMany : List (UnificationGroup l r) -> List (UnificationGroup l r) -> List (UnificationGroup l r)
	mergeMany a b = foldr (\g, us => merge g us []) b a

	total
	add_to_group : Either (DAST l) (DAST r) -> (UnificationGroup l r, List (UnificationGroup l r)) -> (UnificationGroup l r, List (UnificationGroup l r))
	add_to_group e@(Left (ʌ _)) (UnificationGroupV es, us) = (UnificationGroupV (e :: es), us)
	add_to_group e@(Right (ʌ _)) (UnificationGroupV es, us) = (UnificationGroupV (e :: es), us)
	add_to_group e (g, us) =
		let
			UnificationGroupV es = g
		in foldr merger (g, us) $ concatMap (unify_h e) es
		where
			merger : UnificationGroup l r -> (UnificationGroup l r, List (UnificationGroup l r)) -> (UnificationGroup l r, List (UnificationGroup l r))
			merger g' (g, us) =
				case try_merge1 g' g of
					Just (g, us') => (g, mergeMany us us')
					Nothing => (g, merge g' us [])

			total
			unify_h : Either (DAST l) (DAST r) -> Either (DAST l) (DAST r) -> List (UnificationGroup l r)
			unify_h (Left a) (Left b) = map (map $ Left . fromEither) $ unify a b []
			unify_h (Right a) (Right b) = map (map $ Right . fromEither) $ unify a b []
			unify_h (Left a) (Right b) = unify a b []
			unify_h (Right a) (Left b) = map (map mirror) $ unify a b []

	total
	add : DAST l -> DAST r -> List (UnificationGroup l r) -> List (UnificationGroup l r)
	add {l=ln} {r=rn} l r us =
		let
			(gl, us') = find (Left l) us
			(gr, us'') = find (Right r) us'
			f = assert_total $ case catMaybes $ the (List _) [gl, gr] of
				[g1, g2] => add_to_group (Left l) $ add_to_group (Right r) $ do_merge g1 (g2, us'')
				[g] => add_to_group (Left l) $ add_to_group (Right r) $ (g, us'')
				[] => (UnificationGroupV [Left l, Right r], us'')
			(UnificationGroupV g {ne}, us''') = the (UnificationGroup ln rn, List (UnificationGroup ln rn)) f
		in (UnificationGroupV (nub g) {ne = nonEmptyNub ne}) :: us'''

	total
	export
	unify : DAST l -> DAST r -> List (UnificationGroup l r) -> List (UnificationGroup l r)
	unify l r us = assert_total $ unify' (lfreduce l) (lfreduce r) us

	total
	unify' : DAST l -> DAST r -> List (UnificationGroup l r) -> List (UnificationGroup l r)
	unify' l@(ʌ v) r us = add l r us
	unify' l r@(ʌ v) us = add l r us
	unify' (λ lat lb) (λ rat rb) us =
		mergeMany
			(catMaybes $ map pull_group $ unify lb rb [])
			(unify lat rat us)
	unify' (λT lat lrt) (λT rat rrt) us =
		mergeMany
			(catMaybes $ map pull_group $ unify lrt rrt [])
			(unify lat rat us)
	-- unify' (lf =!= la) (rf =!= ra) us = unify lf rf $ unify la ra us
	unify' 𝕋 𝕋 us = us
	unify' (𝔽 lat lrt lb) (𝔽 rat rrt rb) us =
		mergeMany
			(catMaybes $ map (\g => pull_group g >>= pull_group) $ unify lb rb [])
			(mergeMany
				(catMaybes $ map pull_group $ unify lrt rrt [])
				(unify lat rat us)
			)
	unify' l@(𝕌 ln lt) r@(𝕌 rn rt) us =
		if ln == rn
		then unify lt rt us
		else add l r us
	unify' l@(ℂ lc@(DConV {a=la} _ _ _) las) r@(ℂ rc@(DConV {a=ra} _ _ _) ras) us =
		if la == ra && lc == believe_me rc
		then assert_total $ foldr (\f, a => f a) us $ zipWith unify las (believe_me ras)
		else add l r us
	unify' l@(ℙ lv lc@(DConV {a=la} _ _ _) lt lf) r@(ℙ rv rc@(DConV {a=ra} _ _ _) rt rf) us =
		if la == ra && lc == believe_me rc
		then
			mergeMany
				(catMaybes $ map pull_group' $ unify lt (believe_me rt) [])
				(unify lf rf $ unify lv rv us)
		else
			add l r us
	unify' (𝔹 lt) (𝔹 rt) us = unify lt rt us
	unify' l r us = add l r us

total
extract : Either (DAST l) (DAST r) -> (n : Nat ** DAST n)
extract (Left  l) = (_ ** l)
extract (Right r) = (_ ** r)

total
is_similar_h : (n : Nat ** DAST n) -> (n : Nat ** DAST n) -> Bool
is_similar_h (l ** la) (r ** ra) = is_similar la ra

total
export
primary : UnificationGroup l r -> Either (DAST l) (DAST r)
primary (UnificationGroupV es {ne}) =
	case find (either is_concrete is_concrete) $ nubBy (\a, b => is_similar_h (extract a) (extract b)) es of
		Just e => e
		Nothing => head (sortBy p_compare es) {ok = nonEmptySort ne}
	where
		total
		p_compare : Either (DAST l) (DAST r) -> Either (DAST l) (DAST r) -> Ordering
		p_compare (Left (ʌ a)) (Left (ʌ b)) = compare a b
		p_compare (Right (ʌ a)) (Right (ʌ b)) = compare a b
		p_compare (Left _) (Right _) = GT
		p_compare (Right _) (Left _) = LT
		p_compare _ _ = EQ


text:
module Java.Util.Concurrent

import IdrisJvm.FFI

%access public export

namespace TimeUnit
  TimeUnitClass : JVM_NativeTy
  TimeUnitClass = Class "java/util/concurrent/TimeUnit"

  TimeUnit : Type
  TimeUnit = JVM_Native TimeUnitClass

  seconds : TimeUnit
  seconds = unsafePerformIO $ getStaticField TimeUnitClass "SECONDS" (JVM_IO TimeUnit)

  microseconds : TimeUnit
  microseconds = unsafePerformIO $ getStaticField TimeUnitClass "MICROSECONDS" (JVM_IO TimeUnit)

  sleep : TimeUnit -> Bits64 -> JVM_IO ()
  sleep timeunit timeout = invokeInstance "sleep" (TimeUnit -> Bits64 -> JVM_IO ()) timeunit timeout

ext: idr


text:
module Language.Elab.Deriving.DecEq

-- Public: Things here we actually use in deriving DecEq need to be re-exported to
-- be available at the deriving use-site. A little odd but that's how it is.
-- Otherwise you get extremely vague "Can't reify as X" errors and chances are
-- you don't have an FC to track it down.

import public Language.Elab.Syntax
import public Language.Elab.Types

import public Util
import public Language.Elab.Deriving.Util

import public Language.Reflection

import Decidable.Equality

{-
interesting case, happens to work for Show already!
data TagField : Type where
  TF : DecEq a => Show a => (name : String) -> (value : a) -> TagField
-}

-- A regular instance might look like (DecEq a, DecEq b, DecEq c) => ...
-- This pairing isn't actually neccesary, it's just notational convenience and
-- we don't really have a reason to emulate it.
-- DecEq a => DecEq b => ...  is just as valid as (DecEq a, DecEq b) => ...
-- It also can result in clearer errors.
addDecEqAutoImps : List String -> TTImp -> TTImp
addDecEqAutoImps xs retty
  = foldr (\arg,tt => `(DecEq ~(iBindVar arg) => ~(tt))) retty xs

-- I want better names here, including better index names
-- e.g we have this now
{-
Language.Elab.Deriving.DecEq.decEqImplFoo6'Fun : DecEq arg6281 => DecEq arg6282
  => DecEq arg6283 => Foo6' arg6281 arg6282 arg6283 arg6284
    -> Foo6' arg6281 arg6282 arg6283 arg6284 -> Bool
-}

||| e.g. decEq : Foo a b -> Foo a b -> Bool
decEqClaim : (opname : Name) -> TypeInfo -> Visibility -> Elab Decl
decEqClaim op tyinfo vis = do
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      params = map (extractNameStr . name) $ filter (not . isIndex) conargs
      tysig = `((x1 : ~(tyinfo.type)) -> (x2 : ~(tyinfo.type)) -> Dec (x1 = x2))
      tysig' = addDecEqAutoImps params tysig
  logMsg "decEqClaim" 1 $ (show op) ++ (", auto params: ") ++ show params
  logTerm "decEqClaimTySig" 1 "" tysig'
  -- NB: I can't think of a reason not to Inline here
  pure $ iClaim MW vis [Inline] (mkTy op tysig')

-- creates a TTImp that is used for the left hand side. Uses arginfo to determine if should be implicit or explicit
lhsApp : ArgInfo -> TTImp -> TTImp -> TTImp
lhsApp ai caller callee =
       if isImplicitPi (ai.piInfo)
       then iNamedApp caller ai.name callee
       else iApp caller callee

decEqSameCon :
               (funName : Name) -- Name of the function being constructed
               -> (conName : Name) -- Name of the constructor
               -> (argInfos : List ArgInfo)
               -> Elab Clause
decEqSameCon funName conName argInfos =
    let -- for decidable equality, every argument must match (besides indexes) or we can't prove it
      lp = makeLhsPat True
      rp = makeLhsPat False
      lhs = makeLhs lp rp
      rhs = makeRhs lp rp
    in
      do
         logTerm "decEqSameConLhs" 1 "" lhs
         logTerm "decEqSameConRhs" 1 "" rhs
         --logTerm "decEqSameCon" 1 "" lp
         --pure $ patClause lhs `(believe_me) --rhs
         pure $ patClause lhs rhs --(IHole EmptyFC ("samecon" ++ show conname))
         --pure $ patClause lhs (IHole EmptyFC "samecon") --rhs  FIXME
  where
    lVarName : Int -> Name
    lVarName index = UN $ "l" ++ show index
    rVarName : Int -> Name
    rVarName index = UN $ "r" ++ show index
    prfVarName : Int -> Name
    prfVarName index = UN $ "prf" ++ show index

    isArgIndexList : List Bool
    isArgIndexList = map isIndex argInfos

    -- ^ List of whether each argument of the constructor are indexes, in order of the
    --   args as applied to the constructor.
    --   "index" means args that are part of the resulting type, and therefore don't need to be proved
    --   to be equal for the objects to be proven equal
    makeLhsPat : Bool -> TTImp
    makeLhsPat isLeftArg = makeLhsPatHelper (iVar conName) argInfos (rangeFrom 1)
      where
        makeLhsPatHelper : TTImp -> List ArgInfo -> Stream Int -> TTImp
        makeLhsPatHelper innerRes [] _ = innerRes
        makeLhsPatHelper innerRes (ai :: ais) cl@(ctr :: remcl) =
          case isIndex ai of
            True =>
               let res = lhsApp ai innerRes implicit'
               in makeLhsPatHelper res ais cl
               -- ^ regarding vbns: we don't take from the counter stream
               --   Since rhs only uses non-index variables, this way, the var counter
               --   won't skip a value for them
            False =>
              let res = lhsApp ai innerRes (iVar $ (if isLeftArg then lVarName ctr else rVarName ctr))
              in makeLhsPatHelper res ais remcl

    makeLhs : TTImp -> TTImp -> TTImp
    makeLhs lp rp =
      iApp (iApp (iVar funName) lp) rp

    makeRhs : TTImp -> TTImp -> TTImp
    makeRhs lp rp = makeRhsHelper nonIndexVars -- we only deal with the non-index vars
      where
        nonIndexVarCount : Int
        nonIndexVarCount = cast $ length (filter not isArgIndexList)
        nonIndexVars : List Int
        nonIndexVars = if nonIndexVarCount == 0 then [] else [1..nonIndexVarCount]
        makeNoPrf : (v1 : Name) -> (v2 : Name) -> TTImp
        makeNoPrf v1 v2 =
          let
             --all vars on the left and on the right
             allNonIndexVarNames : List Name
             allNonIndexVarNames =
               (map lVarName nonIndexVars) ++ (map rVarName nonIndexVars)
             -- applyCon : Name -> List Name -> TTImp
             -- applyCon con xs = foldl iApp con (map iVar xs)
             foldrFun : Name -> TTImp -> TTImp
             foldrFun otr inner = IPi EmptyFC MW ImplicitArg (Just otr) implicit' inner
             makeNoPrfType : TTImp
             makeNoPrfType =
               --this outer fold is to imply as implicit all the vars used by the proof
               --for some reason, idris gets confused if we don't do this
               foldr foldrFun
                     `((~lp = ~rp) -> (~(iVar v1) === ~(iVar v2)))
                     allNonIndexVarNames
          in
            `(let objEqVarEqPrf : ~makeNoPrfType
            --`(let objEqVarEqPrf : (~(iVar v1) = ~(iVar v2)) -> (~(iVar v1) = (~(iVar v2)))
                  objEqVarEqPrf Refl = Refl
                  -- ^ prf that if two objects are equal
                  -- then the var we're dealing with is equal
              in
                  --contra returns void if v1 = v2
                  --since if first object(o1) = second object(o2), then all its vars must be
                  --equal. So if o1 = o2 then v1 = v2, and contra returns void, so
                  --therefore o1 = o2 implies void and must be false
                  No $ contra . objEqVarEqPrf
            )
        makeYesPrf : TTImp
        makeYesPrf = foldr (\prf,accPrf => `(rewrite (sym ~(prf)) in ~(accPrf))) `(Refl)
                        (map (iVar . prfVarName) nonIndexVars )
        makeRhsHelper : List Int -> TTImp
        makeRhsHelper [] = `(Yes Refl)
        makeRhsHelper (index :: indexes) =
          let v1 = lVarName index
              v2 = rVarName index
              yp = prfVarName index
          in
            iCase `(decEq ~(iVar v1) ~(iVar v2)) `(Dec (_ = _))
                  [patClause `(No contra) (makeNoPrf v1 v2),
                   patClause `(Yes ~(iVar yp))
                                   (case indexes of
                                      Nil => `(Yes ~(makeYesPrf))
                                      _ => makeRhsHelper indexes)
                  ]

decEqDiffCon : (opname : Name) -> Constructor -> Constructor -> Elab Clause
decEqDiffCon op con1 con2 =
  do
    sym1 <- readableGenSym "a"
    sym2 <- readableGenSym "b"
    logMsg "decEqCA1" 1 (show con1.args)
    logMsg "decEqCA2" 1 (show con1.args)
    (let
        pat1 = makePat con1.name sym1 con1.args
        pat2 = makePat con2.name sym2 con2.args
        lhs = iVar op `iApp` pat1 `iApp` pat2
        rhs = makeRhs sym1 sym2
     in
      do
        --logTerm "decEqDiffCon" 1 "" rhs
        pure $ patClause lhs rhs --(IHole EmptyFC ("diffcon" ++ show cn1 ++ show cn2))
     )
  where
    -- The lhs of our function, fields we don't use are replaced with _
    makePat : (con : Name) -> (sym : Name) -> (List ArgInfo) -> TTImp
    makePat con sym argInfos = iAs sym
        (foldl (\tt,ai => lhsApp ai tt implicit') (iVar con) argInfos)
    makeRhs : (sym1 : Name) -> (sym2 : Name) -> TTImp
    makeRhs s1 s2 = `( No (\case Refl impossible))

||| The record that idris would make for you when you write an implementation.
decEqObject : (decname : Name) -> (funname : Name) -> TypeInfo
          -> Visibility -> Elab (Decl, Decl)
decEqObject decname decEqfun tyinfo vis = do
  (qname,_) <- lookupName `{{DecEq}}
  [NS _ (DN _ decEqcon)] <- getCons qname
    | _ => fail "decEqObject: error during DecEq constructor lookup"
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      varnames' = map (show . name) (filter (not . isIndex) conargs)
      retty = `( DecEq ~(appTyCon (map (show . name) conargs)  tyinfo.name))
      tysig = addDecEqAutoImps varnames' retty
      claim = iClaim MW vis [Hint True] (mkTy decname tysig)
      rhs = `( ~(iVar decEqcon) ~(iVar decEqfun))
      body = iDef decname [(patClause (iVar decname) rhs)]
  pure $ (claim,body)

export
||| Usage: %runElab deriveDecEq Export `{{Foo}}
||| Currently, this adds decDecEqImplFoo (a function that returns the "interface" data object and marks itself
||| as with hint on, and decDecEqImpltFooFun which actually implements decDecEq.
||| This is likely to change in the future to only have decDecEqImplFoo being added
||| to the namespace.
deriveDecEq : Visibility -> Name -> Elab ()
deriveDecEq vis decEqname = do
    (qname,_) <- lookupName decEqname -- get the qualified name of our type
    -- create human readable names for our instance components
    let decn = mapName (\d => "decEqImpl" ++ d) decEqname
        funn = mapName (\d => "decEqImpl" ++ d ++ "Fun") decEqname
    -- Build general info about the type we're deriving (e.g. Foo) that we want
    -- to keep around.
    tyinfo <- makeTypeInfo qname

    -- The components of our decEq-ing function
    funclaim <- decEqClaim funn tyinfo Private -- NB private

    traverse (\con =>
      do
        logMsg "deriveDecEq" 1 $ "con name : " ++ show con.name
        logMsg "deriveDecEq" 1 $ "con list args: " ++ show con.args
        logTerm "deriveDecEq" 1 "contype: " con.type
      ) tyinfo.cons

    funSameClauses <- traverse (\con => decEqSameCon funn con.name con.args) tyinfo.cons
    let diffCons = filter (not . isSameCons) [ (a,b) | a <- tyinfo.cons, b <- tyinfo.cons ]
    funDiffClauses <- traverse (uncurry $ decEqDiffCon funn) diffCons

    -- Our function's complete definition
    let fundecl = iDef funn (funSameClauses ++ funDiffClauses)

    -- The actual decEqImplFoo : DecEq Foo record.
    (objclaim,objclause) <- decEqObject decn funn tyinfo vis

    -- Declare our things into the namespace
    -- Both claims first, otherwise we won't find our own DecEq in fundecl
    declare [funclaim, objclaim]
    declare [fundecl, objclause]
 where
   isSameCons : (Constructor, Constructor) -> Bool
   isSameCons (con1, con2) = con1.name == con2.name


text:
module WordsProvider

import Data.String

-- split lines
readLines : String -> List String
readLines content = let words = Strings.split (\c => List.elem c ['\n', '\r']) content in
                        filter (/= "") words

export
readWords : String -> IO (Provider (List String))
readWords fileName = do maybeFile <- readFile fileName
                        pure $ case maybeFile of
                                       Left error => Error $ "Failed to load seo words: " ++ show error
                                       Right content => Provide (readLines content)

max_stars_repo_name: janschultecom/typelevel-seo

max_issues_repo_name: janschultecom/typelevel-seo

max_forks_repo_name: janschultecom/typelevel-seo


text:
import Data.Vect

{- 1 -}

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

testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [0, 0, 0]]

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
import Control.Monad.State

increase : Nat -> State Nat ()
increase inc = do current <- get
                  put (current + inc)


text:
module Collections.BSTree.Set

import Collections.BSTree.Map as M
import Collections.BSTree.Set.Core
import Collections.BSTree.Set.Quantifiers
import Collections.Util.Bnd
import Data.Nat
import Data.Nat.Order.Strict
import Decidable.Order.Strict

import public Collections.BSTree.Set.Core

------------------
-- CONSTRUCTION --
------------------

||| The empty tree.
public export
empty : {0 sto : kTy -> kTy -> Type} ->
        {auto pre : StrictPreorder kTy sto} ->
        {auto tot : StrictOrdered kTy sto} ->
        BSTree sto {pre} {tot}
empty = M.empty

||| A tree with a single element.
public export
singleton : {0 sto : kTy -> kTy -> Type} ->
            {auto pre : StrictPreorder kTy sto} ->
            {auto tot : StrictOrdered kTy sto} ->
            (k : kTy) ->
            BSTree sto {pre} {tot}
singleton k = M.singleton k ()

---------------
-- INSERTION --
---------------

||| Insert an element in a tree. If the tree already contains an element equal to the given value,
||| it is replaced with the new value.
export
insert : {0 sto : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy sto} ->
         {tot : StrictOrdered kTy sto} ->
         (k : kTy) ->
         BSTree sto {pre} {tot} ->
         BSTree sto {pre} {tot}
insert k t = M.insert k () t

--------------
-- QUERYING --
--------------

||| Is the tree empty?
export
null : BSTree sto {pre} {tot} -> Bool
null = M.null

||| The number of elements in the tree.
export
size : BSTree sto {pre} {tot} -> Nat
size = M.size

||| Is the element in the tree?
export
member : {0 sto : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy sto} ->
         {tot : StrictOrdered kTy sto} ->
         (k : kTy) ->
         BSTree sto {pre} {tot} ->
         Bool
member = M.member

-----------------------
-- DELETION / UPDATE --
-----------------------

||| Delete an element from a tree. When the element is not in the tree, the original tree is
||| returned.
export
delete : {0 sto : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy sto} ->
         {tot : StrictOrdered kTy sto} ->
         (k : kTy) ->
         BSTree sto {pre} {tot} ->
         BSTree sto {pre} {tot}
delete = M.delete

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
module Collections.Util.Erased

||| A data type which wraps an erased value, so that it can be returned by a function for use in
||| another erased context.
public export
data Erased : (0 t : Type) -> Type where
  MkErased : (0 x : t) -> Erased t


text:
module Main

import Test.Golden

%default covering

-- To add more tests, copy one of the test directories, then update this list
examples : TestPool
examples =
  MkTestPool "Examples: Idris -> Cairo -> Output"
    [] Default
    [ "test001", "test002", "test003", "test004", "test005",
      "test006", "test007", "test008", "test009", "test010",
      "test011", "test012", "test013", "test014", "test015"]

primitiveTests : TestPool
primitiveTests = MkTestPool "'Tests' Primops"
    [] Default
    [ "felt", "uint", "int"]

main : IO ()
main = runner
  [ testPaths "idrisToCairo/examples" examples,
    testPaths "idrisToCairo/primitives" primitiveTests
  ] where
    testPaths : String -> TestPool -> TestPool
    testPaths dir = { testCases $= map ((dir ++ "/") ++) }

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Hangman

import Data.Vect
import Pred

data GameState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
     MkGameState : (word : String)
                   -> (missing : Vect letters Char)
                   -> GameState guesses_remaining letters

data Finished : Type where
     Lost : (game : GameState 0 (S letters)) -> Finished
     Won : (game : GameState (S guesses) 0) -> Finished

data ValidInput : List Char -> Type where
     Letter : (c : Char) -> ValidInput [c]

processGuess : (letter : Char) ->
               GameState (S guesses) (S letters) ->
               Either (GameState guesses (S letters)) (GameState (S guesses) letters)
processGuess letter (MkGameState word missing)
                = case isElem letter missing of
                       Yes prf => Right (MkGameState word (removeElem_auto letter missing))
                       No contra => Left (MkGameState word missing)

isValidInput : (cs : List Char) -> Dec (ValidInput cs)

isValidString : (s : String) -> Dec (ValidInput (unpack s))

readGuess : IO (x ** ValidInput x)
readGuess = do putStr "Guess:"
               x <- getLine
               case isValidString (toUpper x) of
                    Yes prf => pure (_ ** prf)
                    No contra => do putStrLn "Invalid guess"
                                    readGuess

game : GameState (S guesses) (S letters) -> IO Finished
game st = ?game_rhs


text:
module Test.Pipes

import Control.Monad.Writer
import Pipes
import Test.Utils

%access export

--------------------------------------------------------------------------------
-- Pure pipelines
--------------------------------------------------------------------------------

even : Int -> Bool
even n = mod n 2 == 0

test_filtering_mapping : Test
test_filtering_mapping = do
  let ints = each [1..10] .| filtering even .| mapping (*2)
  assertEq 60 $ runPure (ints .| summing)
  assertEq 122880 $ runPure (ints .| multiplying)

test_iterating_take : Test
test_iterating_take = do
  assertEq 55 $ runPure $ iterating (+1) 1 .| taking 10 .| summing
  assertEq 55 $ runPure $ iterating (+1) 1 .| takingWhile (< 11) .| summing

test_unfolding_drop : Test
test_unfolding_drop = do
  let source = unfolding (\x => Just (x, x + 1)) (-9)
  assertEq 55 $ runPure $ source .| dropping 10 .| taking 10 .| summing
  assertEq 55 $ runPure $ source .| droppingWhile (< 1) .| taking 10 .| summing

test_repeating_deduplicating : Test
test_repeating_deduplicating = do
  assertEq 110 $ runPure $ each [1..10] .| repeating 2 .| summing
  assertEq 55 $ runPure $ each [1..10] .| repeating 2 .| deduplicating .| summing

test_concatMapping : Test
test_concatMapping = do
  assertEq 110 $ runPure $ each [1..10] .| concatMapping (\x => [x, x]) .| summing

test_grouping : Test
test_grouping = do
  assertEq [2, 4, 6, 8, 10] $
    runPure (each [1..5] .| repeating 2 .| grouping .| mapping sum .| consuming)

test_chunking : Test
test_chunking = do
  assertEq [[1, 2], [3, 4], [5]] $
    runPure (each [1..5] .| chunking 2 .| consuming)

test_splitting : Test
test_splitting = do
  assertEq [[1], [3], [5]] $
    runPure (each [1..5] .| splittingBy even .| consuming)

test_replicating_scanning : Test
test_replicating_scanning = do
  assertEq [0..10] $
    runPure (replicating 10 1 .| scanning (+) 0 .| consuming)

--------------------------------------------------------------------------------
-- Effectful pipes
--------------------------------------------------------------------------------

test_tracing : Test
test_tracing = do
  (a, w) <- runWriterT $ runPipe (each [1..10] .| tracing (tell . show) .| discard)
  assertEq "12345678910" w

rightOr : r -> Either l r -> r
rightOr r (Left _) = r
rightOr _ (Right r) = r

test_reading_file : Test
test_reading_file = do
  r <- runPipe (readFile "./Test/test.txt" .| mapping (rightOr "") .| consuming)
  assertEq "123\n45678\n9\n" (concat r)

earlyTerminating : MonadWriter String m => Source m String
earlyTerminating = do
  yieldOr "." (tell "done")
  earlyTerminating

test_early_termination : Test
test_early_termination = do
  (a, w) <- runWriterT $ runPipe (earlyTerminating .| taking 10 .| discard)
  assertEq "done" w

--------------------------------------------------------------------------------
-- All tests
--------------------------------------------------------------------------------

run_tests : IO ()
run_tests = runTestSuite
    [ test_filtering_mapping
    , test_iterating_take
    , test_unfolding_drop
    , test_repeating_deduplicating
    , test_concatMapping
    , test_grouping
    , test_chunking
    , test_splitting
    , test_replicating_scanning
    , test_tracing
    , test_reading_file
    , test_early_termination
    ]

--

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


text:
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

Eq Shape where
  (==) (Triangle w h) (Triangle w' h') =
    w == w' && h == h'
  (==) (Rectangle w h) (Rectangle w' h') =
    w == w' && h == h'
  (==) (Circle r) (Circle r') =
    r == r'
  (==) _ _ = False

Ord Shape where
  compare first second = compare (area first) (area second)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture
%name Shape shape, shape1, shape2
%name Picture pic, pic1, pic2

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)
circle : Picture
circle = Primitive (Circle 5)
triangle : Picture
triangle = Primitive (Triangle 10 10)
triangle2 : Picture
triangle2 = Primitive (Triangle 100 10)

test_picture : Picture
test_picture = Combine (Combine (Translate 5 5 rectangle)
                  (Combine (Translate 35 5 circle) (Translate 15 25 triangle))) (Translate 20 20 triangle2)

picture_area : Picture -> Double
picture_area (Primitive shape) = area shape
picture_area (Combine pic1 pic2) = picture_area pic1 + picture_area pic2
picture_area (Rotate x pic) = picture_area pic
picture_area (Translate x y pic) = picture_area pic

safe_divide : Double -> Double -> Maybe Double
safe_divide x 0.0 = Nothing
safe_divide x y = Just (x / y)

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe (Just x) (Just y) = case compare x y of
                                  LT => Just y
                                  EQ => Just x
                                  GT => Just x

biggestTriangle_helper : (p : Picture) -> (size : Maybe Double) -> Maybe Double
biggestTriangle_helper (Primitive tri @ (Triangle x y)) Nothing = Just (area tri)
biggestTriangle_helper (Primitive tri @ (Triangle x y)) right_size @ (Just z) = let left_size = Just (area tri) in
                                                                                maxMaybe left_size right_size
biggestTriangle_helper (Primitive (Rectangle x y)) size = size
biggestTriangle_helper (Primitive (Circle x)) size = size
biggestTriangle_helper (Combine left right) size = let left_size = biggestTriangle_helper left size
                                                       right_size = biggestTriangle_helper right size in
                                                       maxMaybe (maxMaybe left_size right_size) size
biggestTriangle_helper (Rotate x pic) size = biggestTriangle_helper pic size
biggestTriangle_helper (Translate x y pic) size = biggestTriangle_helper pic size

biggestTriangle : Picture -> Maybe Double
biggestTriangle p = biggestTriangle_helper p Nothing

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
-- ----------------------------------------------------------- [ AbsInterp.idr ]
-- Module    : AbsInterp.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.Builder.AbsInterp

import Effects
import Effect.State

import Data.AVL.Dict

import GRL.Lang.GLang
import GRL.Eval

import Sif.Types
import Sif.Pattern
import Sif.Builder.Utils

-- -------------------------------------------------------------- [ Directives ]

%access private
%default partial

-- ----------------------------------------- [ Private Internal Data Structure ]

data AbsInterpPriv : InterpRes ty -> SifTy -> Type where
  PrivmkReq : (ty   : RTy)
             -> (t    : String)
             -> (desc : Maybe String)
             -> AbsInterpPriv (interpReq t) tyREQ

  PrivmkProb : (title : String)
              -> (desc  : Maybe String)
              -> DList (InterpRes TyREQ) (\x => AbsInterpPriv x TyREQ) xs
              -> AbsInterpPriv (interpProb title xs) TyPROBLEM

  PrivmkTLink : (cval : CValue)
               -> (req : AbsInterpPriv r TyREQ)
               -> (desc : Maybe String)
               -> AbsInterpPriv (interpAffect cval r) TyAFFECTS

  PrivmkTrait : (ty : TTy)
               -> (title : String)
               -> (desc  : Maybe String)
               -> (sval  : SValue)
               -> DList (InterpRes TyAFFECTS) (\x => AbsInterpPriv x TyAFFECTS) rs
               -> AbsInterpPriv (interpTrait title sval rs ty) TyTRAIT

  PrivmkProp : (title : String)
              -> (desc : Maybe String)
              -> DList (InterpRes TyTRAIT) (\x => AbsInterpPriv x TyTRAIT) ts
              -> AbsInterpPriv (interpProp title ts) TyPROPERTY

  PrivmkSolt : (title : String)
              -> (desc : Maybe String)
              -> DList (InterpRes TyPROPERTY) (\x => AbsInterpPriv x TyPROPERTY) ps
              -> AbsInterpPriv (interpSolt title ps) TySOLUTION

  PrivmkPatt : (title : String)
              -> (desc : Maybe String)
              -> AbsInterpPriv p TyPROBLEM
              -> AbsInterpPriv s TySOLUTION
              -> AbsInterpPriv (interpPatt p s) TyPATTERN

-- ----------------------------------------------------- [ Instances and Stuff ]

getModel : {x : InterpRes TyPATTERN} -> AbsInterpPriv x TyPATTERN -> GModel
getModel {x} _ = extract x
  where
    extract : InterpRes TyPATTERN -> GModel
    extract (IPatt m) = m
    extract _         = emptyModel

-- ------------------------------------------------------ [ Builder Definition ]

evalPatternAbs : {i : InterpRes TyPATTERN}
              -> AbsInterpPriv i TyPATTERN
              -> Sif.EvalResult
evalPatternAbs p =
    case evalModel (getModel p) Nothing of
      BadModel  => Bad
      Result gs => Good $ map (\x => (getNodeTitle x, getSValue x)) (getGNodes gs)

-- Technically, cheating by not propagating the domain across the
-- inner inner type but it is okay IMHO.
export
data AbsInterpRep : SifTy -> SifDomain -> Type where
  MkWrapper : {i : InterpRes ty} -> AbsInterpPriv i ty -> AbsInterpRep ty d

-- --------------------------------------------------------------- [ Interface ]

getPrivTitle : AbsInterpPriv i ty -> {auto prf : HasMData ty} -> String
getPrivTitle (PrivmkReq _ t _)       = t
getPrivTitle (PrivmkProb t _ _)      = t
getPrivTitle (PrivmkTrait _ t _ _ _) = t
getPrivTitle (PrivmkProp t _ _)      = t
getPrivTitle (PrivmkSolt t _ _)      = t
getPrivTitle (PrivmkPatt t _ _ _)    = t
getPrivTitle _ = "Error"

getPrivDesc : AbsInterpPriv i ty -> Maybe String
getPrivDesc (PrivmkReq _ _ d)       = d
getPrivDesc (PrivmkProb _ d rs)     = d
getPrivDesc (PrivmkTLink _ _ d)     = d
getPrivDesc (PrivmkTrait _ _ d _ _) = d
getPrivDesc (PrivmkProp _ d _)      = d
getPrivDesc (PrivmkSolt _ d _)      = d
getPrivDesc (PrivmkPatt _ d _ _)    = d
getPrivDesc _ = Nothing

getPrivRTy : {i : InterpRes TyREQ}
          -> AbsInterpPriv i TyREQ
          -> RTy
getPrivRTy (PrivmkReq ty _ _) = ty

getPrivTTy : {i : InterpRes TyTRAIT}
          -> AbsInterpPriv i TyTRAIT
          -> TTy
getPrivTTy (PrivmkTrait ty _ _ _ _) = ty

getPrivSValue : {i : InterpRes TyTRAIT}
              -> AbsInterpPriv i TyTRAIT
              -> SValue
getPrivSValue (PrivmkTrait _ _ _ sval as) = sval

getPrivCValue : {i : InterpRes TyAFFECTS}
             -> AbsInterpPriv i TyAFFECTS
             -> CValue
getPrivCValue (PrivmkTLink cval _ _) = cval

getPrivProblem : {i : InterpRes TyPATTERN}
              -> AbsInterpPriv i TyPATTERN
              -> (x : InterpRes TyPROBLEM ** AbsInterpPriv x TyPROBLEM)
getPrivProblem (PrivmkPatt _ _ p _) = (_ ** p)

getPrivSolution : {i : InterpRes TyPATTERN}
               -> AbsInterpPriv i TyPATTERN
               -> (s : InterpRes TySOLUTION ** AbsInterpPriv s TySOLUTION)
getPrivSolution (PrivmkPatt _ _ _ s) = (_ ** s)

getPrivReqs : {i : InterpRes TyPROBLEM}
            -> AbsInterpPriv i TyPROBLEM
            -> (xs ** DList (InterpRes TyREQ) (\x => AbsInterpPriv x TyREQ) xs)
getPrivReqs (PrivmkProb _ _ rs) = (_ ** rs)

getPrivProperties : {i : InterpRes TySOLUTION}
                  -> AbsInterpPriv i TySOLUTION
                  -> (xs ** DList (InterpRes TyPROPERTY) (\x => AbsInterpPriv x TyPROPERTY) xs)
getPrivProperties (PrivmkSolt _ _ ps) = (_ ** ps)

getPrivTraits : {i : InterpRes TyPROPERTY}
             -> AbsInterpPriv i TyPROPERTY
             -> (xs ** DList (InterpRes TyTRAIT) (\x => AbsInterpPriv x TyTRAIT) xs)
getPrivTraits (PrivmkProp _ _ ts) = (_ ** ts)

getPrivAffects : {i : InterpRes TyTRAIT}
               -> AbsInterpPriv i TyTRAIT
               -> (xs ** DList (InterpRes TyAFFECTS) (\x => AbsInterpPriv x TyAFFECTS) xs)
getPrivAffects (PrivmkTrait _ _ _ _ as) = (_ ** as)

getPrivReq : {i : InterpRes TyAFFECTS}
          -> AbsInterpPriv i TyAFFECTS
          -> (s : InterpRes TyREQ ** AbsInterpPriv s TyREQ)
getPrivReq (PrivmkTLink _ r _) = (_ ** r)

SifRepAPI AbsInterpRep where
  getTitle  (MkWrapper i) = getPrivTitle i
  getDesc   (MkWrapper i) = getPrivDesc  i
  getTTy    (MkWrapper x) = getPrivTTy x
  getRTy    (MkWrapper x) = getPrivRTy x
  getSValue (MkWrapper x) = getPrivSValue x
  getCValue (MkWrapper x) = getPrivCValue x

  getProblem    (MkWrapper x) = MkWrapper $ snd $ getPrivProblem x
  getSolution   (MkWrapper x) = MkWrapper $ snd $ getPrivSolution x

  getReqs       (MkWrapper x) = map (\(prf ** i) => MkWrapper i) $ toLDP $  (snd  (getPrivReqs x))
  getProperties (MkWrapper x) = map (\(prf ** i) => MkWrapper i) $ toLDP $  (snd  (getPrivProperties x))
  getTraits     (MkWrapper x) = map (\(prf ** i) => MkWrapper i) $ toLDP $  (snd  (getPrivTraits x))
  getAffects    (MkWrapper x) = map (\(prf ** i) => MkWrapper i) $ toLDP $ (snd (getPrivAffects x))
  getReq        (MkWrapper x) = MkWrapper $ snd $ getPrivReq x

  evalPattern (MkWrapper p)    = evalPatternAbs p
  fetchMetaModel (MkWrapper p) = m
      where
        g : GModel
        g = getModel p

        m : MetaModel
        m = mkMetaModel g

-- ------------------------------------------------------------- [ The Builder ]

covering
buildReqAbs : (d : SifDomain)
           -> RTy
           -> String
           -> Maybe String
           -> REQUIREMENT AbsInterpRep d
buildReqAbs _ ty s d = MkExpr $ MkWrapper $ PrivmkReq ty s d

%inline covering
convS : List (SifExpr ty d AbsInterpRep)
    -> (xs : List (InterpRes ty) ** DList (InterpRes ty) (\x => AbsInterpPriv x ty) xs)
convS xs = fromLDP $ map (\(MkExpr (MkWrapper x)) => (_ ** x)) xs

%inline covering
conv : {ty : SifTy}
    -> SifExpr ty d AbsInterpRep
    -> (r : InterpRes ty ** AbsInterpPriv r ty)
conv (MkExpr (MkWrapper res)) = (_ ** res)

covering
buildProblemAbs : (d : SifDomain)
               -> String
               -> Maybe String
               -> REQUIREMENTS AbsInterpRep d
               -> PROBLEM AbsInterpRep d
buildProblemAbs c t d rs =
    MkExpr $ MkWrapper $ PrivmkProb t d (snd $ convS rs)

covering
buildAffectAbs : (d : SifDomain)
              -> CValue
              -> REQUIREMENT AbsInterpRep d
              -> Maybe String
              -> AFFECT AbsInterpRep d
buildAffectAbs _ c r d =
    MkExpr $ MkWrapper $ PrivmkTLink c
           (snd $ conv r) d

covering
buildTraitAbs : (d : SifDomain)
             -> TTy
             -> String
             -> Maybe String
             -> SValue
             -> AFFECTS AbsInterpRep d
             -> TRAIT AbsInterpRep d
buildTraitAbs _ ty t d s rs =
    MkExpr $ MkWrapper $ PrivmkTrait ty t d s (snd $ convS rs)

covering
buildPropertyAbs : (d : SifDomain)
                -> String
                -> Maybe String
                -> TRAITS AbsInterpRep d
                -> PROPERTY AbsInterpRep d
buildPropertyAbs _ t d ts =
    MkExpr $ MkWrapper $ PrivmkProp t d (snd $ convS ts)

covering
buildSolutionAbs : (d : SifDomain)
                -> String
                -> Maybe String
                -> PROPERTIES AbsInterpRep d
                -> SOLUTION AbsInterpRep d
buildSolutionAbs _ s d ps =
    MkExpr $ MkWrapper $ PrivmkSolt s d
           (snd $ convS ps)

covering
buildPatternAbs : (d : SifDomain)
               -> String
               -> Maybe String
               -> PROBLEM AbsInterpRep  d
               -> SOLUTION AbsInterpRep d
               -> PATTERN AbsInterpRep  d
buildPatternAbs _ t d (MkExpr (MkWrapper p)) (MkExpr (MkWrapper s)) =
    MkExpr $ MkWrapper $ PrivmkPatt t d p s

covering
export
absInterpBuilder : SifBuilder AbsInterpRep
absInterpBuilder = MkSifBuilder
    buildReqAbs
    buildProblemAbs
    buildAffectAbs
    buildTraitAbs
    buildPropertyAbs
    buildSolutionAbs
    buildPatternAbs

covering
export
backendAbsInterp : SifBackend
backendAbsInterp = MkBackend "interp" absInterpBuilder

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
> module Fun.MathExpr

from https://github.com/DSLsofMath/DSLsofMath/blob/master/L/DSLsofMath/FunExp.lhs

> import Interfaces.Math

> %default total
> %access public export
> %auto_implicits on -- off

> ||| Functions as expressions
> data MathExpr : Type -> Type where
>   Id    : MathExpr t
>   Neg   : MathExpr t
>   Exp   : MathExpr t
>   Sin   : MathExpr t
>   Cos   : MathExpr t
>   Const : t -> MathExpr t
>   (+)   : MathExpr t -> MathExpr t -> MathExpr t
>   (-)   : MathExpr t -> MathExpr t -> MathExpr t
>   (*)   : MathExpr t -> MathExpr t -> MathExpr t
>   (/)   : MathExpr t -> MathExpr t -> MathExpr t
>   (.)   : MathExpr t -> MathExpr t -> MathExpr t

> ||| Evaluation
> eval : (Num t, Fractional t, Neg t, Math t) => MathExpr t -> t -> t
> eval Id        x = id x
> eval Neg       x = - x
> eval Exp       x = exp x
> eval Sin       x = sin x
> eval Cos       x = cos x
> eval (Const c) x = (const c) x
> eval (e1 + e2) x = (eval e1 x) + (eval e2 x)
> eval (e1 - e2) x = (eval e1 x) - (eval e2 x)
> eval (e1 * e2) x = (eval e1 x) * (eval e2 x)
> eval (e1 / e2) x = (eval e1 x) / (eval e2 x)
> eval (e1 . e2) x = (eval e1 (eval e2 x))

> ||| Differentiation
> derivative : (Num t, Fractional t, Neg t) => MathExpr t -> MathExpr t
> derivative Id        = Const 1
> derivative Neg       = Const (negate 1)
> derivative Exp       = Exp
> derivative Sin       = Cos
> derivative Cos       = Neg . Sin
> derivative (Const c) = Const 0
> derivative (e1 + e2) = derivative e1 + derivative e2
> derivative (e1 - e2) = derivative e1 - derivative e2
> derivative (e1 * e2) = (derivative e1) * e2 + e1 * (derivative e2)
> derivative (e1 / e2) = (derivative e1) / e2 - e1 * (derivative e2) / (e2 * e2)
> derivative (e1 . e2) = ((derivative e1) . e2) * (derivative e2)

This needs to be tested!

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
foo : String
foo = """
  \{show 1}
    """


text:
module Server.InigoServer.Util

import Data.Either
import Data.String
import Inigo.Async.Base
import Inigo.Async.CloudFlare.Worker
import Inigo.Async.Promise
import Inigo.Package.PackageIndex
import Server.Template.Template

export
renderLayout : String -> String -> String
renderLayout layout contents =
  if layout == "" then -- Allow empty or missing layout
    contents
  else
    template layout [("CONTENTS", contents)]

export
sniffContentType : String -> Headers
sniffContentType path =
  if isSuffixOf ".css" path
    then [("Content-Type", "text/css")]
    else if isSuffixOf ".svg" path
      then [("Content-Type", "image/svg+xml")]
      else []

export
withIndex : String -> String
withIndex "/" = "/home"
withIndex s = s

export
buildPkgLink : PackageMeta -> String
buildPkgLink (MkPackageMeta ns package description version) =
  let
    qualifiedName = ns ++ "." ++ package
    packagePath = "/packages/" ++ ns ++ "/" ++ package
    desc = case description of
      Just d =>
        " - " ++ d

      Nothing =>
        ""
  in
    " * [" ++ qualifiedName ++ "](" ++ packagePath ++ ")" ++ desc

||| Helpful default function for kv which returns empty strings
export
def : a -> (String -> a) -> String -> a
def d f "" = d
def d f str = f str

||| Raise an Either to a promise of its right prong
export
expectResult : Show err => Either err a -> Promise a
expectResult (Right x) = lift x
expectResult (Left err) = reject (show err)

||| Raise an Either to a promise of its right prong
export
expect : Show err => err -> Maybe a -> Promise a
expect err x = expectResult (maybeToEither err x)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Tools.Annotation

import Tools.Indexed
import Tools.AstF

%access public export

AstFTy : Type -> Type
AstFTy idx = (idx -> Type) -> (idx -> Type)

data Annotated : (idx : Type) -> (f : AstFTy idx)
              -> (i : idx) -> (ann : Type) -> Type where
  Ann : (a : ann) -> f (\id => Annotated idx f id ann) i -> Annotated idx f i ann

AstF idx f => IxFunctor idx (Annotated idx f) where
  imap {b} {a} {i} fn (Ann x rec) = Ann (fn x)
                          $ localMap (\id => Annotated idx f id a)
                                     (\id => Annotated idx f id b)
                                     (\id => imap {i = id} fn)
                                     i rec

AstF idx f => IxCopointed idx (Annotated idx f) where
  iextract (Ann x _) = x


text:
module Stream'

f : Type -> Type
f _ = Nat

corecord Stream' : Type -> Type where
  hd : Stream' a -> a
  tl : Stream' (id a) -> Stream' a
  constructor (::)

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module Replica.App.Format

import public Control.ANSI
import Control.App

import Replica.Option.Global
import Replica.App.Log
import Replica.App.Replica
import Replica.Other.Decorated

export
ok : State GlobalConfig Global e => App e String
ok = do
  ascii <- map ascii $ get GlobalConfig
  pure $ if ascii then "OK " else "✅ "

export
ko : State GlobalConfig Global e => App e String
ko = do
  ascii <- map ascii $ get GlobalConfig
  pure $ if ascii then "KO " else "❌ "

export
err : State GlobalConfig Global e => App e String
err = do
  ascii <- map ascii $ get GlobalConfig
  pure $ if ascii then "ERR" else "⚠ "

export
pending : State GlobalConfig Global e => App e String
pending = do
  ascii <- map ascii $ get GlobalConfig
  pure $ if ascii then "ZzZ" else "💤"

export
qmark : State GlobalConfig Global e => App e String
qmark = do
  ascii <- map ascii $ get GlobalConfig
  pure $ if ascii then "?" else "❓"

export
bold : State GlobalConfig Global e => App e (String -> String)
bold = do
  c <- map colour $ get GlobalConfig
  pure $ if c then (show . bolden) else id

export
yellow : State GlobalConfig Global e => App e (String -> String)
yellow = do
  c <- map colour $ get GlobalConfig
  pure $ if c then (show . colored Yellow) else id

export
green : State GlobalConfig Global e => App e (String -> String)
green = do
  c <- map colour $ get GlobalConfig
  pure $ if c then (show . colored Green) else id

export
red : State GlobalConfig Global e => App e (String -> String)
red = do
  c <- map colour $ get GlobalConfig
  pure $ if c then (show . colored Red) else id

export
blue : State GlobalConfig Global e => App e (String -> String)
blue = do
  c <- map colour $ get GlobalConfig
  pure $ if c then (show . colored BrightBlue) else id

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Primes

import NatUtils
import gcd
import Data.Fin
import NatOrder
import SriramAssRecRule

%access public export
%default total

--isDivisible a b can be constucted if b divides a
isDivisible : Nat -> Nat -> Type
isDivisible a b = (n : Nat ** (GT n 0, a = b * n))

--1 divides everything
oneDiv : (a : Nat) -> {auto x : GT a 0} -> isDivisible a 1
oneDiv a {x=pf} = (a ** (pf , rewrite plusZeroRightNeutral a in Refl))

--If 1|a => 1*c | a*c
mulDiv : (a, c : Nat) -> {auto pf1 : GT a 0} -> {auto pf2 : GT c 0} ->
  isDivisible a 1 -> isDivisible (a * c) c
mulDiv a c {pf1=p} x = (a ** (p ,rewrite multCommutative a c in Refl))

--Either(a=b)(_) <=> Either (S a = S b)(_)
help1 : {a : Nat} -> {b : Nat} ->
  Either (a = b) (Either (LT (S a) (S b)) (LT (S b) (S a))) ->
  Either (S a = S b) (Either (LT (S a) (S b)) (LT (S b) (S a)))
help1 {a} {b} (Left l) = Left (eqSucc a b l)
help1 (Right r) = Right r

--Either(_)(Either(Sa<Sb)(_)) <=> Either (_)(Either(a<b)(_))
help2 : {a : Nat} -> {b : Nat} ->
  Either (a = b) (Either (LT a b) (LT (S b) (S a))) ->
  Either (a = b) (Either (LT (S a) (S b)) (LT (S b) (S a)))
help2 (Left l) = Left l
help2 {a} {b} (Right (Left l)) = Right(Left (LTESucc l))
help2 (Right (Right r)) = Right (Right r)

--Either(_)(Either(_)(Sb<Sa)) <=> Either (_)(Either(_)(b<a))
help3 : {a : Nat} -> {b : Nat} ->
  Either (a = b) (Either (LT a b) (LT b a)) ->
  Either (a = b) (Either (LT a b) (LT (S b) (S a)))
help3 (Left l) = Left l
help3 (Right (Left l)) = Right(Left l)
help3 {a} {b} (Right (Right r)) = Right (Right (LTESucc r))

|||Either a = b, a < b, or a > b
totOrdNat : (a : Nat) -> (b : Nat) ->
  Either (a = b) (Either (LT a b) (LT b a))
totOrdNat Z Z = Left Refl
totOrdNat Z (S k) = Right (Left (LTESucc LTEZero))
totOrdNat (S k) Z = Right (Right (LTESucc LTEZero))
totOrdNat (S k) (S j) = help1 (help2 (help3 (totOrdNat k j)))

--LTE a b => LTE a*n b*n
multRightLTE : (a,b : Nat) -> (n : Nat) -> GT n 0 ->
  LTE a b -> LTE (a*n) (b*n)
multRightLTE a b (S Z) (LTESucc LTEZero) lteab =
                            rewrite multOneRightNeutral a in
                            rewrite multOneRightNeutral b in
                            lteab
multRightLTE a b (S (S k)) (LTESucc LTEZero{right=(S k)}) lteab =
          rewrite multRightSuccPlus a (S k) in
          rewrite multRightSuccPlus b (S k) in
          ltePlusIsLTE lteab
          (multRightLTE a b (S k) (LTESucc LTEZero{right=k}) lteab)

--If a = b*n, b <= a
aEqProdImpAGtB : (a,b,n : Nat) -> GT n 0 -> (a = b*n) -> LTE b a
aEqProdImpAGtB _ _ Z LTEZero _ impossible
aEqProdImpAGtB _ _ Z (LTESucc _) _ impossible
aEqProdImpAGtB (b * (S k)) b (S k) x Refl = case b of
              Z => LTEZero
              (S m) =>
                rewrite sym (multOneLeftNeutral (S m)) in
                rewrite multCommutative (S m) (S k) in
                rewrite multDistributesOverPlusRight k (S Z) m in
                rewrite plusCommutative (k*1) (k*m) in
                rewrite plusAssociative m (k*m) (k*1) in
                rewrite plusCommutative (m + k*m) (k*1) in
                rewrite sym (multDistributesOverPlusRight (S k) 1 m) in
                multRightLTE 1 (S k) (S m) (LTESucc (LTEZero)) x

--If b | a => b <= a
bDivAImpAGtB : (a,b,n : Nat) -> isDivisible a b -> LTE b a
bDivAImpAGtB a b n (x ** pf) = case (fst pf) of
              (LTESucc LTEZero{right=k}) => aEqProdImpAGtB a b (S k) (fst pf) (snd pf)

--GT implies Not LTE
gtImpliesNotLTE : GT a b -> Not (LTE a b)
gtImpliesNotLTE {a=Z} {b=_} LTEZero impossible
gtImpliesNotLTE {a=Z} {b=_} (LTESucc _) impossible
gtImpliesNotLTE {a=(S k)} {b=Z} x = case isLTE (S k) Z of
                                 (Yes prf) => absurd
                                 (No contra) => contra
gtImpliesNotLTE {a=(S k)} {b=(S j)} x = case isLTE (S k) (S j) of
                                 (Yes prf) => void
                                      (gtImpliesNotLTE (fromLteSucc x) (fromLteSucc prf))
                                 (No contra) => contra

--If b > a => b does not divide a
bGtAImpNotbDivA : (a,b,n : Nat) -> GT b a -> (isDivisible a b -> Void)
bGtAImpNotbDivA a b n x = impliesContrapositive
                          (isDivisible a b)
                          (LTE b a)
                          (bDivAImpAGtB a b n)
                          (gtImpliesNotLTE x)

--(S (S k)) = 0 is not possible
zNotEqSS : (k : Nat) -> ((S (S k)) = 0 -> Void)
zNotEqSS Z = absurd
zNotEqSS (S k) = absurd

--isDivisible p 0 => (S (S k)) = 0
help4 : (p : Nat) -> LTE 2 p -> isDivisible p 0 -> p = 0
help4 Z LTEZero _ impossible
help4 Z (LTESucc _) _ impossible
help4 (S Z) (LTESucc LTEZero) _ impossible
help4 (S Z) (LTESucc (LTESucc _)) _ impossible
help4 (S (S k)) (LTESucc (LTESucc LTEZero)) x = snd (snd x)

--If x = 0, and p >= 2, x cannot divide p
zNotDivp : (p : Nat) -> LTE 2 p -> ((isDivisible p 0) -> Void)
zNotDivp Z LTEZero impossible
zNotDivp Z (LTESucc _) impossible
zNotDivp (S Z) (LTESucc LTEZero) impossible
zNotDivp (S Z) (LTESucc (LTESucc _)) impossible
zNotDivp (S (S k)) (LTESucc (LTESucc LTEZero)) =
                        impliesContrapositive
                        (isDivisible (S (S k)) 0)
                        ((S (S k)) = 0)
                        (help4 (S (S k)) (LTESucc (LTESucc LTEZero)))
                        (zNotEqSS k)

-- Helping out metaHelp
metaMetaHelp5 : (j : Nat) -> (S (j+0)) = (S j)
metaMetaHelp5 Z = Refl
metaMetaHelp5 (S k) = rewrite plusZeroRightNeutral k in Refl

--Helping out help5
metaHelp5 : (S (S k)) = (S (j+0)) -> (S (S k)) = (S (j))
metaHelp5 {j} prf = rewrite sym (metaMetaHelp5 j) in prf

-- Helping out the absurd case
help5: (S (S k)) = (S (j+0)) -> LT (S j) (S (S k)) ->  LTE (S Z) 0
help5 {k} {j} prf x = lteMinusConstantRight {c=(S j)}
            (rewrite sym (metaMetaHelp5 j) in
             rewrite sym prf in
             rewrite eqSucc (S (S k)) (S j) (metaHelp5 prf) in
             x)

--If a divides b => b=a*n
bDivAImpBEqAN : (a,b : Nat) -> isDivisible b a ->  (k : Nat ** b = a * k)
bDivAImpBEqAN a b (p ** (proofGT, proofEq)) = (p ** proofEq)

--To help out help6
metaHelp6 : (p : Nat) -> (x : Nat) -> (c : Nat) ->
  (p = x*c) -> q = c -> (p = q*x)
metaHelp6 p x c prf prf1 = rewrite prf1 in
                       rewrite multCommutative c x in prf

--To help out a case in notDivIfRem
help6 : (p : Nat) -> (x : Nat) -> (c : Nat) ->
  (p = q*x) -> (p = (S r) + q*x) ->
  (Z = (S r))
help6 p x c {q} {r} p1 p2 = plusRightCancel Z (S r) (q*x) (trans (sym p1) p2)

--To help out another case of notDivIfRem
help7 : (p : Nat) -> (x : Nat) -> (c : Nat) -> (k : Nat) -> (r : Nat) ->
        c + k = q -> p = x*c -> p = (S r) + q*x ->
        Z = (S r) + k*x
help7 p x c k r pfSum pfMul pfRem =
          plusRightCancel Z ((S r)+k*x) (c*x)
          (rewrite sym (plusAssociative (S r) (k*x) (c*x)) in
           rewrite plusCommutative (k*x) (c*x) in
           rewrite sym (multDistributesOverPlusLeft c k x) in
           rewrite pfSum in
           rewrite sym (multCommutative x c) in
           rewrite sym (pfMul) in pfRem)

--Helper for help8
metahelp8 : (x : Nat) -> (S q) + k = c -> x +(q+k)*x = c*x
metahelp8 x prf = rewrite sym prf in Refl

--Last case!
help8 : (p : Nat) -> (x : Nat) -> (c : Nat) -> (k : Nat) ->
        (m : Nat) -> (r : Nat) -> (q : Nat) ->
        (S q) + k = c -> (S (S r)) + m = x -> p = x*c -> p = (S r) + q*x ->
        Z = k*(S r) + (S k)*(S m)
help8 p x c k m r q qLtc srLtx pfMul pfRem =
          plusLeftCancel (S r) Z (k*(S r) + (S k)*(S m))
          (rewrite plusAssociative (S r) (k*(S r)) ((S k)*(S m)) in
           rewrite sym (multDistributesOverPlusRight (S k) (S r) (S m)) in
           rewrite plusAssociative r (S Z) m in
           rewrite plusCommutative r (S Z) in
           rewrite srLtx in
           rewrite sym (plusCommutative (k*x) ((S (S r)) + m)) in
           rewrite srLtx in
           rewrite plusCommutative (k*x) x in
           rewrite plusZeroRightNeutral r in
           plusLeftCancel (q*x) (S r) (x + k*x)
           (rewrite plusAssociative (q*x) x (k*x) in
            rewrite plusCommutative (q*x) x in
            rewrite sym (multDistributesOverPlusLeft (S q) k x) in
            rewrite metahelp8 {q=q} {k=k} {c=c} x qLtc in
            rewrite (multCommutative c x) in
            rewrite sym pfMul in
            rewrite plusCommutative (q*x) (S r) in
            (sym pfRem)))

help9 : (k,r,m : Nat) ->
        Z = k*(S r) + (S k)*(S m) -> Z = (S k)*(S m) + k*(S r)
help9 k r m prf = rewrite plusCommutative ((S k)*(S m)) (k*(S r)) in prf

--To help out the last case, by creating a term of an uninhabited type
notDivIfRem : (p : Nat) -> (x : Nat) -> (r : Nat) -> {q : Nat} ->
  (p = (S r) + q*x) -> LT (S r) x ->
  (c : Nat ** p = x * c) -> Void
notDivIfRem p x r {q=q} prfRem prfLt (c ** prfDiv) =
    case decEq q c of
        (Yes prf) => absurd $
                      (help6 p x c (metaHelp6 p x c prfDiv prf) prfRem)
        (No contra) => case totOrdNat q c of
              (Left l) => void (contra l)
              (Right (Left qLtc)) => case (lteToLEQ qLtc) of
                        (k ** pf1) => case (lteToLEQ prfLt) of
                          (m ** pf2) => absurd $
                              help9 k r m
                                (help8 p x c k m r q pf1 pf2 prfDiv prfRem)
              (Right (Right qGtc)) => case (lteToLEQ (lteSuccLeft qGtc)) of
                          (k ** pf) => absurd $
                              (help7 p x c k r pf prfDiv prfRem)

--The usual case for divisibility
usual : (p : Nat) -> LTE 2 p -> (x : Nat) -> (LT 0 x) -> (LT x p) ->
  (euc : (q : Nat ** (r : Nat ** ((p = r + (q * x)), LT r x)))) ->
  Dec (isDivisible p x)
usual Z LTEZero _ _ _ _ impossible
usual Z (LTESucc _) _ _ _ _ impossible
usual (S Z) (LTESucc LTEZero) _ _ _ _ impossible
usual (S Z) (LTESucc (LTESucc _)) _ _ _ _ impossible
usual (S (S _)) (LTESucc (LTESucc LTEZero)) Z LTEZero _ _ impossible
usual (S (S _)) (LTESucc (LTESucc LTEZero)) Z (LTESucc _) _ _ impossible
usual (S (S k)) (LTESucc (LTESucc LTEZero))
      (S j) (LTESucc LTEZero)
      xLtp euc with (euc)
        usual (S (S k)) (LTESucc (LTESucc LTEZero))
              (S j) (LTESucc LTEZero)
              xLtp euc | (Z ** (Z ** (pf,_))) = absurd $ pf

        usual (S (S k)) (LTESucc (LTESucc LTEZero))
              (S j) (LTESucc LTEZero)
              xLtp euc | ((S Z) ** (Z ** (pf,_))) = absurd $
                      (help5 pf xLtp)

        usual (S (S k)) (LTESucc (LTESucc LTEZero))
              (S j) (LTESucc LTEZero)
              xLtp euc | ((S (S b)) ** (Z ** (pf,_))) =
                Yes ((S (S b)) ** ((LTESucc LTEZero),
                                    (rewrite multCommutative (S j) (S (S b)) in pf)))

        usual (S (S k)) (LTESucc (LTESucc LTEZero))
              (S j) (LTESucc LTEZero)
              xLtp euc | (_ ** ((S a) ** (pf1,pf2))) = No
                              (impliesContrapositive
                                (isDivisible (S (S k)) (S j))
                                (c : Nat ** (S (S k)) = (S j) * c)
                                (bDivAImpBEqAN (S j) (S (S k)))
                                (notDivIfRem (S (S k)) (S j) a pf1 pf2))

--Decidability for divisibility
decDiv : (p : Nat) -> LTE 2 p -> (x : Nat) ->
  {euc : (q : Nat ** (r : Nat ** ((p = r + (q * x)), LT r x)))} ->
  Dec (isDivisible p x)
decDiv Z LTEZero _ impossible
decDiv Z (LTESucc _) _ impossible
decDiv (S Z) (LTESucc LTEZero) _ impossible
decDiv (S Z) (LTESucc (LTESucc _)) _ impossible
decDiv (S (S k)) (LTESucc (LTESucc LTEZero)) x {euc=big} =
    case totOrdNat (S (S k)) x of
      (Left l) => Yes (1 ** ((LTESucc LTEZero),
                             rewrite l in
                             rewrite sym (multOneRightNeutral x) in
                             Refl))
      (Right (Left l)) => No (bGtAImpNotbDivA
                              (S (S k)) x
                              (divNatNZ x (S (S k)) SIsNotZ)
                              l)
      (Right (Right r)) => case x of
          Z => No (zNotDivp (S (S k)) (LTESucc (LTESucc LTEZero)))
          (S m) => usual (S (S k)) (LTESucc (LTESucc LTEZero)) (S m)
                   (LTESucc LTEZero) r big


text:
import Specdris.Spec

import Document
import Cursor

firstLine : String
firstLine = " line"

filename : String
filename = "afile"

oneLiner : Document
oneLiner = MkDocument [firstLine] filename

secondLine : String
secondLine = " line2"

twoLiner : Document
twoLiner = MkDocument [firstLine, secondLine] filename

main : IO ()
main = spec $ do
  describe "document" $ do
    describe "insert" $ do
      describe "single line" $ do
        it "adds a single character to the beginning" $ do
          (insert oneLiner (MkCursor Z Z) 'a') `shouldBe` (MkDocument ["a line"] filename)

        it "adds a single character to the middle" $ do
          (insert oneLiner (MkCursor (S Z) Z) 'a') `shouldBe` (MkDocument [" aline"] filename)

        it "adds a single character to the end" $ do
          (insert oneLiner (MkCursor (length firstLine) Z) 'a') `shouldBe` (MkDocument [" linea"] filename)

      describe "multiple lines" $ do
        it "adds a single character to the first line" $ do
          (insert twoLiner (MkCursor Z Z) 'a') `shouldBe` (MkDocument ["a line", secondLine] filename)

        it "adds a single character to the second line" $ do
          (insert twoLiner (MkCursor Z (S Z)) 'a') `shouldBe` (MkDocument [firstLine, "a line2"] filename)

      describe "cursor after bounds" $ do
        it "should not edit after the end of a line" $ do
          (insert oneLiner (MkCursor (1 + length firstLine) Z) 'a') `shouldBe` oneLiner

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
module Solutions.Prim

import Data.Bits
import Data.DPair
import Data.List
import Data.Maybe
import Data.SnocList
import Decidable.Equality

%default total

--------------------------------------------------------------------------------
--          Working with Strings
--------------------------------------------------------------------------------

-- 1

map : (Char -> Char) -> String -> String
map f = pack . map f . unpack

filter : (Char -> Bool) -> String -> String
filter f = pack . filter f . unpack

mapMaybe : (Char -> Maybe Char) -> String -> String
mapMaybe f = pack . mapMaybe f . unpack

-- 2

foldl : (a -> Char -> a) -> a -> String -> a
foldl f v = foldl f v . unpack

foldMap : Monoid m => (Char -> m) -> String -> m
foldMap f = foldMap f . unpack

-- 3

traverse : Applicative f => (Char -> f Char) -> String -> f String
traverse fun = map pack . traverse fun . unpack

-- 4
(>>=) : String -> (Char -> String) -> String
str >>= f = foldMap f $ unpack str

--------------------------------------------------------------------------------
--          Integers
--------------------------------------------------------------------------------

-- 1

record And a where
  constructor MkAnd
  value : a

Bits a => Semigroup (And a) where
  MkAnd x <+> MkAnd y = MkAnd $ x .&. y

Bits a => Monoid (And a) where
  neutral = MkAnd oneBits

-- 2

record Or a where
  constructor MkOr
  value : a

Bits a => Semigroup (Or a) where
  MkOr x <+> MkOr y = MkOr $ x .|. y

Bits a => Monoid (Or a) where
  neutral = MkOr zeroBits

-- 3

even : Bits64 -> Bool
even x = not $ testBit x 0

-- 4

binChar : Bits64 -> Char
binChar x = if testBit x 0 then '1' else '0'

toBin : Bits64 -> String
toBin 0 = "0"
toBin v = go [] v
  where go : List Char -> Bits64 -> String
        go cs 0 = pack cs
        go cs v = go (binChar v :: cs) (assert_smaller v $ v `shiftR` 1)

-- 5

-- Note: We know that `x .&. 15` must be a value in the range
-- [0,15] (unless there is a bug in the backend we use), but since
-- `Bits64` is a primitive, Idris can't know this. We therefore
-- fail with a runtime crash in the impossible case, but annotate the
-- call to `idris_crash` with `assert_total` (otherwise, `hexChar` would
-- be a partial function).
hexChar : Bits64 -> Char
hexChar x = case x .&. 15 of
  0  => '0'
  1  => '1'
  2  => '2'
  3  => '3'
  4  => '4'
  5  => '5'
  6  => '6'
  7  => '7'
  8  => '8'
  9  => '9'
  10 => 'a'
  11 => 'b'
  12 => 'c'
  13 => 'd'
  14 => 'e'
  15 => 'f'
  x  => assert_total $ idris_crash "IMPOSSIBLE: Invalid hex digit (\{show x})"

toHex : Bits64 -> String
toHex 0 = "0"
toHex v = go [] v
  where go : List Char -> Bits64 -> String
        go cs 0 = pack cs
        go cs v = go (hexChar v :: cs) (assert_smaller v $ v `shiftR` 4)

--------------------------------------------------------------------------------
--          Refined Primitives
--------------------------------------------------------------------------------

data Dec0 : (prop : Type) -> Type where
  Yes0 : (0 prf : prop) -> Dec0 prop
  No0  : (0 contra : prop -> Void) -> Dec0 prop

data IsYes0 : (d : Dec0 prop) -> Type where
  ItIsYes0 : IsYes0 (Yes0 prf)

0 fromYes0 : (d : Dec0 prop) -> (0 prf : IsYes0 d) => prop
fromYes0 (Yes0 x) = x
fromYes0 (No0 contra) impossible

interface Decidable (0 a : Type) (0 p : a -> Type) | p where
  decide : (v : a) -> Dec0 (p v)

decideOn : (0 p : a -> Type) -> Decidable a p => (v : a) -> Dec0 (p v)
decideOn _ = decide

test0 : (b : Bool) -> Dec0 (b === True)
test0 True  = Yes0 Refl
test0 False = No0 absurd

0 unsafeDecideOn : (0 p : a -> Type) -> Decidable a p => (v : a) -> p v
unsafeDecideOn p v = case decideOn p v of
  Yes0 prf => prf
  No0  _   =>
    assert_total $ idris_crash "Unexpected refinement failure in `unsafeRefineOn`"

0 safeDecideOn :  (0 p : a -> Type)
               -> Decidable a p
               => (v : a)
               -> (0 prf : IsYes0 (decideOn p v))
               => p v
safeDecideOn p v = fromYes0 $ decideOn p v

-- 1

{x : a} -> DecEq a => Decidable a (Equal x) where
  decide v = case decEq x v of
    Yes prf   => Yes0 prf
    No contra => No0 contra

-- 2

data Neg : (p : a -> Type) -> a -> Type where
  IsNot : {0 p : a -> Type} -> (contra : p v -> Void) -> Neg p v

Decidable a p => Decidable a (Neg p) where
  decide v = case decideOn p v of
    Yes0 prf   => No0 $ \(IsNot contra) => contra prf
    No0 contra => Yes0 $ IsNot contra

-- 3

data (&&) : (p,q : a -> Type) -> a -> Type where
  Both : {0 p,q : a -> Type} -> (prf1 : p v) -> (prf2 : q v) -> (&&) p q v

Decidable a p => Decidable a q => Decidable a (p && q) where
  decide v = case decideOn p v of
    Yes0 prf1 => case decideOn q v of
      Yes0 prf2   => Yes0 $ Both prf1 prf2
      No0  contra => No0 $ \(Both _ prf2) => contra prf2
    No0  contra => No0 $ \(Both prf1 _) => contra prf1

-- 4

data (||) : (p,q : a -> Type) -> a -> Type where
  L : {0 p,q : a -> Type} -> (prf : p v) -> (p || q) v
  R : {0 p,q : a -> Type} -> (prf : q v) -> (p || q) v

Decidable a p => Decidable a q => Decidable a (p || q) where
  decide v = case decideOn p v of
    Yes0 prf1    => Yes0 $ L prf1
    No0  contra1 => case decideOn q v of
      Yes0 prf2    => Yes0 $ R prf2
      No0  contra2 => No0 $ \case L prf => contra1 prf
                                  R prf => contra2 prf

-- 5

negOr : Neg (p || q) v -> (Neg p && Neg q) v
negOr (IsNot contra) = Both (IsNot $ contra . L) (IsNot $ contra . R)

andNeg : (Neg p && Neg q) v -> Neg (p || q) v
andNeg (Both (IsNot c1) (IsNot c2)) =
  IsNot $ \case L p1 => c1 p1
                R p2 => c2 p2

orNeg : (Neg p || Neg q) v -> Neg (p && q) v
orNeg (L (IsNot contra)) = IsNot $ \(Both p1 _) => contra p1
orNeg (R (IsNot contra)) = IsNot $ \(Both _ p2) => contra p2

0 negAnd :  Decidable a p
         => Decidable a q
         => Neg (p && q) v
         -> (Neg p || Neg q) v
negAnd (IsNot contra) = case decideOn p v of
  Yes0 p1 => case decideOn q v of
    Yes0 p2 => void (contra $ Both p1 p2)
    No0 c   => R $ IsNot c
  No0 c    => L $ IsNot c

-- 6

data (<=) : (m,n : Nat) -> Type where
  ZLTE : 0 <= n
  SLTE : m <= n -> S m <= S n

(>=) : (m,n : Nat) -> Type
m >= n = n <= m

(<) : (m,n : Nat) -> Type
m < n = S m <= n

(>) : (m,n : Nat) -> Type
m > n = n < m

LessThan : (m,n : Nat) -> Type
LessThan m = (< m)

To : (m,n : Nat) -> Type
To m = (<= m)

GreaterThan : (m,n : Nat) -> Type
GreaterThan m = (> m)

From : (m,n : Nat) -> Type
From m = (>= m)

FromTo : (lower,upper : Nat) -> Nat -> Type
FromTo l u = From l && To u

Between : (lower,upper : Nat) -> Nat -> Type
Between l u = GreaterThan l && LessThan u

Uninhabited (S n <= 0) where
  uninhabited ZLTE impossible
  uninhabited (SLTE _) impossible

0 fromLTE : (n1,n2 : Nat) -> (n1 <= n2) === True -> n1 <= n2
fromLTE 0     n2    prf = ZLTE
fromLTE (S k) (S j) prf = SLTE $ fromLTE k j prf
fromLTE (S k) 0     prf = absurd prf

0 toLTE : (n1,n2 : Nat) -> n1 <= n2 -> (n1 <= n2) === True
toLTE 0     0     _        = Refl
toLTE 0     (S k) _        = Refl
toLTE (S k) (S j) (SLTE x) = toLTE k j x
toLTE (S k) 0     x        = absurd x

{n : Nat} -> Decidable Nat (<= n) where
  decide m = case test0 (m <= n) of
    Yes0 prf   => Yes0 $ fromLTE m n prf
    No0 contra => No0 $ contra . toLTE m n

{m : Nat} -> Decidable Nat (m <=) where
  decide n = case test0 (m <= n) of
    Yes0 prf   => Yes0 $ fromLTE m n prf
    No0 contra => No0 $ contra . toLTE m n

-- 7

0 refl : {n : Nat} -> n <= n
refl {n = 0}   = ZLTE
refl {n = S _} = SLTE refl

0 trans : {l,m,n : Nat} -> l <= m -> m <= n -> l <= n
trans {l = 0}   _        _        = ZLTE
trans {l = S _} (SLTE x) (SLTE y) = SLTE $ trans x y

0 (>>) : {l,m,n : Nat} -> l <= m -> m <= n -> l <= n
(>>) = trans

-- 8

0 toIsSucc : {n : Nat} -> n > 0 -> IsSucc n
toIsSucc {n = S _} (SLTE _) = ItIsSucc

0 fromIsSucc : {n : Nat} -> IsSucc n -> n > 0
fromIsSucc {n = S _} ItIsSucc = SLTE ZLTE

-- 9

safeDiv : (x,y : Bits64) -> (0 prf : cast y > 0) => Bits64
safeDiv x y = x `div` y

safeMod :  (x,y : Bits64)
        -> (0 prf : cast y > 0)
        => Subset Bits64 (\v => cast v < cast y)
safeMod x y = Element (x `mod` y) (unsafeDecideOn (<= cast y) _)

-- 10

digit : (v : Bits64) -> (0 prf : cast v < 16) => Char
digit 0  = '0'
digit 1  = '1'
digit 2  = '2'
digit 3  = '3'
digit 4  = '4'
digit 5  = '5'
digit 6  = '6'
digit 7  = '7'
digit 8  = '8'
digit 9  = '9'
digit 10 = 'a'
digit 11 = 'b'
digit 12 = 'c'
digit 13 = 'd'
digit 14 = 'e'
digit 15 = 'f'
digit x  = assert_total $ idris_crash "IMPOSSIBLE: Invalid digit (\{show x})"

record Base where
  constructor MkBase
  value : Bits64
  0 prf : FromTo 2 16 (cast value)

base : Bits64 -> Maybe Base
base v = case decideOn (FromTo 2 16) (cast v) of
  Yes0 prf => Just $ MkBase v prf
  No0  _   => Nothing

namespace Base
  public export
  fromInteger : (v : Integer) -> {auto 0 _ : IsJust (base $ cast v)} -> Base
  fromInteger v = fromJust $ base (cast v)

digits : Bits64 -> Base -> String
digits 0 _ = "0"
digits x (MkBase b $ Both p1 p2) = go [] x
  where go : List Char -> Bits64 -> String
        go cs 0 = pack cs
        go cs v =
          let Element d p = (v `safeMod` b) {prf = %search >> p1}
              v2          = (v `safeDiv` b) {prf = %search >> p1}
           in go (digit d {prf = p >> p2} :: cs) (assert_smaller v v2)

-- 11

data CharOrd : (p : Nat -> Type) -> Char -> Type where
  IsCharOrd : {0 p : Nat -> Type} -> (prf : p (cast c)) -> CharOrd p c

Decidable Nat p => Decidable Char (CharOrd p) where
  decide c = case decideOn p (cast c) of
    Yes0 prf   => Yes0 $ IsCharOrd prf
    No0 contra => No0 $ \(IsCharOrd prf) => contra prf

-- 12

IsAscii : Char -> Type
IsAscii = CharOrd (< 128)

IsLatin : Char -> Type
IsLatin = CharOrd (< 255)

IsUpper : Char -> Type
IsUpper = CharOrd (FromTo (cast 'A') (cast 'Z'))

IsLower : Char -> Type
IsLower = CharOrd (FromTo (cast 'a') (cast 'z'))

IsAlpha : Char -> Type
IsAlpha = IsUpper || IsLower

IsDigit : Char -> Type
IsDigit = CharOrd (FromTo (cast '0') (cast '9'))

IsAlphaNum : Char -> Type
IsAlphaNum = IsAlpha || IsDigit

IsControl : Char -> Type
IsControl = CharOrd (FromTo 0 31 || FromTo 127 159)

IsPlainAscii : Char -> Type
IsPlainAscii = IsAscii && Neg IsControl

IsPlainLatin : Char -> Type
IsPlainLatin = IsLatin && Neg IsControl

-- 12

0 plainToAscii : IsPlainAscii c -> IsAscii c
plainToAscii (Both prf1 _) = prf1

0 digitToAlphaNum : IsDigit c -> IsAlphaNum c
digitToAlphaNum = R

0 alphaToAlphaNum : IsAlpha c -> IsAlphaNum c
alphaToAlphaNum = L

0 lowerToAlpha : IsLower c -> IsAlpha c
lowerToAlpha = R

0 upperToAlpha : IsUpper c -> IsAlpha c
upperToAlpha = L

0 lowerToAlphaNum : IsLower c -> IsAlphaNum c
lowerToAlphaNum = L . R

0 upperToAlphaNum : IsUpper c -> IsAlphaNum c
upperToAlphaNum = L . L

0 asciiToLatin : IsAscii c -> IsLatin c
asciiToLatin (IsCharOrd x) = IsCharOrd (trans x $ safeDecideOn _ _)

0 plainAsciiToPlainLatin : IsPlainAscii c -> IsPlainLatin c
plainAsciiToPlainLatin (Both x y) = Both (asciiToLatin x) y

-- 13

data Head : (p : a -> Type) -> List a -> Type where
  AtHead : {0 p : a -> Type} -> (0 prf : p v) -> Head p (v :: vs)

Uninhabited (Head p []) where
  uninhabited (AtHead _) impossible

Decidable a p => Decidable (List a) (Head p) where
  decide []        = No0 $ \prf => absurd prf
  decide (x :: xs) = case decide {p} x of
    Yes0 prf    => Yes0 $ AtHead prf
    No0  contra => No0 $ \(AtHead prf) => contra prf

-- 14

data Length : (p : Nat -> Type) -> List a -> Type where
  HasLength :  {0 p : Nat -> Type}
            -> (0 prf : p (List.length vs))
            -> Length p vs

Decidable Nat p => Decidable (List a) (Length p) where
  decide vs = case decideOn p (length vs) of
    Yes0 prf   => Yes0 $ HasLength prf
    No0 contra => No0 $ \(HasLength prf) => contra prf

-- 15

data All : (p : a -> Type) -> (as : List a) -> Type where
  Nil  : All p []
  (::) :  {0 p : a -> Type}
       -> (0 h : p v)
       -> (0 t : All p vs)
       -> All p (v :: vs)

data AllSnoc : (p : a -> Type) -> (as : SnocList a) -> Type where
  Lin  : AllSnoc p [<]
  (:<) :  {0 p : a -> Type}
       -> (0 i : AllSnoc p vs)
       -> (0 l : p v)
       -> AllSnoc p (vs :< v)

0 head : All p (x :: xs) -> p x
head (h :: _) = h

0 (<>>) : AllSnoc p sx -> All p xs -> All p (sx <>> xs)
(<>>) [<]      y = y
(<>>) (i :< l) y = i <>> l :: y

0 suffix : (sx : SnocList a) -> All p (sx <>> xs) -> All p xs
suffix [<]       x = x
suffix (sx :< y) x = let (_ :: t) = suffix {xs = y :: xs} sx x in t

0 notInner :  {0 p : a -> Type}
           -> (sx : SnocList a)
           -> (0 contra : (prf : p x) -> Void)
           -> (0 prfs : All p (sx <>> x :: xs))
           -> Void
notInner sx contra prfs = let prfs2 = suffix sx prfs in contra (head prfs2)

allTR : {0 p : a -> Type} -> Decidable a p => (as : List a) -> Dec0 (All p as)
allTR as = go Lin as
  where go : (0 sp : AllSnoc p sx) -> (xs : List a) -> Dec0 (All p (sx <>> xs))
        go sp []        = Yes0 $ sp <>> Nil
        go sp (x :: xs) = case decide {p} x of
          Yes0 prf    => go (sp :< prf) xs
          No0  contra => No0 $ \prf => notInner sx contra prf

Decidable a p => Decidable (List a) (All p) where decide = allTR

-- 16

0 IsIdentChar : Char -> Type
IsIdentChar = IsAlphaNum || Equal '_'

0 IdentChars : List Char -> Type
IdentChars = Length (<= 100) && Head IsAlpha && All IsIdentChar

record Identifier where
  constructor MkIdentifier
  value : String
  0 prf : IdentChars (unpack value)

identifier : String -> Maybe Identifier
identifier s = case decideOn IdentChars (unpack s) of
  Yes0 prf => Just $ MkIdentifier s prf
  No0  _   => Nothing

namespace Identifier
  public export
  fromString :  (s : String)
             -> (0 _ : IsYes0 (decideOn IdentChars (unpack s)))
             => Identifier
  fromString s = MkIdentifier s (fromYes0 $ decide (unpack s))

testIdent : Identifier
testIdent = "fooBar_123"


text:
module Text.Parser

import Data.Bool.Extra
import Data.List
import Data.Nat

import public Text.Parser.Core
import public Text.Quantity
import public Text.Token

%default total

||| Parse a terminal based on a kind of token.
export
match : (Eq k, TokenKind k) =>
        (kind : k) ->
        Grammar (Token k) True (TokType kind)
match k = terminal "Unrecognised input" $
    \t => if t.val.kind == k
             then Just $ tokValue k t.val.text
             else Nothing

||| Optionally parse a thing, with a default value if the grammar doesn't
||| match. May match the empty input.
export
option : {c : Bool} ->
         (def : a) -> (p : Grammar tok c a) ->
         Grammar tok False a
option {c = False} def p = p <|> pure def
option {c = True} def p = p <|> pure def

||| Optionally parse a thing.
||| To provide a default value, use `option` instead.
export
optional : {c : Bool} ->
           (p : Grammar tok c a) ->
           Grammar tok False (Maybe a)
optional p = option Nothing (map Just p)

||| Try to parse one thing or the other, producing a value that indicates
||| which option succeeded. If both would succeed, the left option
||| takes priority.
export
choose : {c1, c2 : Bool} ->
         (l : Grammar tok c1 a) ->
         (r : Grammar tok c2 b) ->
         Grammar tok (c1 && c2) (Either a b)
choose l r = map Left l <|> map Right r

||| Produce a grammar by applying a function to each element of a container,
||| then try each resulting grammar until the first one succeeds. Fails if the
||| container is empty.
export
choiceMap : {c : Bool} ->
            (a -> Grammar tok c b) ->
            Foldable t => t a ->
            Grammar tok c b
choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
                                               f x <|> acc)
                           (fail "No more options") xs

%hide Prelude.(>>=)

||| Try each grammar in a container until the first one succeeds.
||| Fails if the container is empty.
export
choice : Foldable t =>
         {c : Bool} ->
         t (Grammar tok c a) ->
         Grammar tok c a
choice = choiceMap id

mutual
  ||| Parse one or more things
  export
  some : Grammar tok True a ->
         Grammar tok True (List a)
  some p = pure (!p :: !(many p))

  ||| Parse zero or more things (may match the empty input)
  export
  many : Grammar tok True a ->
         Grammar tok False (List a)
  many p = option [] (some p)

||| Parse one or more instances of `p`, returning the parsed items and proof
||| that the resulting list is non-empty.
export
some' : (p : Grammar tok True a) ->
        Grammar tok True (xs : List a ** NonEmpty xs)
some' p = pure (!p :: !(many p) ** IsNonEmpty)

mutual
  private
  count1 : (q : Quantity) ->
           (p : Grammar tok True a) ->
           Grammar tok True (List a)
  count1 q p = do x <- p
                  seq (count q p)
                      (\xs => pure (x :: xs))

  ||| Parse `p`, repeated as specified by `q`, returning the list of values.
  export
  count : (q : Quantity) ->
          (p : Grammar tok True a) ->
          Grammar tok (isSucc (min q)) (List a)
  count (Qty Z Nothing) p = many p
  count (Qty Z (Just Z)) _ = pure []
  count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p
  count (Qty (S min) Nothing) p = count1 (atLeast min) p
  count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"
  count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p

mutual
  ||| Parse one or more instances of `p` until `end` succeeds, returning the
  ||| list of values from `p`. Guaranteed to consume input.
  export
  someTill : {c : Bool} ->
             (end : Grammar tok c e) ->
             (p : Grammar tok True a) ->
             Grammar tok True (List a)
  someTill {c} end p = do x <- p
                          seq (manyTill end p)
                              (\xs => pure (x :: xs))

  ||| Parse zero or more instances of `p` until `end` succeeds, returning the
  ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
  export
  manyTill : {c : Bool} ->
             (end : Grammar tok c e) ->
             (p : Grammar tok True a) ->
             Grammar tok c (List a)
  manyTill {c} end p = rewrite sym (andTrueNeutral c) in
                               map (const []) end <|> someTill end p

||| Parse one or more instances of `p` until `end` succeeds, returning the
||| list of values from `p`, along with a proof that the resulting list is
||| non-empty.
export
someTill' : {c : Bool} ->
            (end : Grammar tok c e) ->
            (p : Grammar tok True a) ->
            Grammar tok True (xs : List a ** NonEmpty xs)
someTill' end p
  = do x <- p
       seq (manyTill end p)
           (\xs => pure (x :: xs ** IsNonEmpty))

mutual
  ||| Parse one or more instance of `skip` until `p` is encountered,
  ||| returning its value.
  export
  afterSome : {c : Bool} ->
              (skip : Grammar tok True s) ->
              (p : Grammar tok c a) ->
              Grammar tok True a
  afterSome skip p = do skip
                        afterMany skip p

  ||| Parse zero or more instance of `skip` until `p` is encountered,
  ||| returning its value.
  export
  afterMany : {c : Bool} ->
              (skip : Grammar tok True s) ->
              (p : Grammar tok c a) ->
              Grammar tok c a
  afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
                                 p <|> afterSome skip p

||| Parse one or more things, each separated by another thing.
export
sepBy1 : {c : Bool} ->
         (sep : Grammar tok True s) ->
         (p : Grammar tok c a) ->
         Grammar tok c (List a)
sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
                           [| p :: many (sep *> p) |]

||| Parse zero or more things, each separated by another thing. May
||| match the empty input.
export
sepBy : {c : Bool} ->
        (sep : Grammar tok True s) ->
        (p : Grammar tok c a) ->
        Grammar tok False (List a)
sepBy sep p = option [] $ sepBy1 sep p

||| Parse one or more instances of `p` separated by `sep`, returning the
||| parsed items and proof that the resulting list is non-empty.
export
sepBy1' : {c : Bool} ->
         (sep : Grammar tok True s) ->
         (p : Grammar tok c a) ->
         Grammar tok c (xs : List a ** NonEmpty xs)
sepBy1' {c} sep p
  = rewrite sym (orFalseNeutral c) in
            seq p (\x => do xs <- many (sep *> p)
                            pure (x :: xs ** IsNonEmpty))

||| Parse one or more instances of `p` separated by and optionally terminated by
||| `sep`.
export
sepEndBy1 : {c : Bool} ->
            (sep : Grammar tok True s) ->
            (p : Grammar tok c a) ->
            Grammar tok c (List a)
sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
                              sepBy1 sep p <* optional sep

||| Parse zero or more instances of `p`, separated by and optionally terminated
||| by `sep`. Will not match a separator by itself.
export
sepEndBy : {c : Bool} ->
           (sep : Grammar tok True s) ->
           (p : Grammar tok c a) ->
           Grammar tok False (List a)
sepEndBy sep p = option [] $ sepEndBy1 sep p

||| Parse zero or more instances of `p`, separated by and optionally terminated
||| by `sep`, returning the parsed items and a proof that the resulting list
||| is non-empty.
export
sepEndBy1' : {c : Bool} ->
             (sep : Grammar tok True s) ->
             (p : Grammar tok c a) ->
             Grammar tok c (xs : List a ** NonEmpty xs)
sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in
                               sepBy1' sep p <* optional sep

||| Parse one or more instances of `p`, separated and terminated by `sep`.
export
endBy1 : {c : Bool} ->
         (sep : Grammar tok True s) ->
         (p : Grammar tok c a) ->
         Grammar tok True (List a)
endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in
                                  p <* sep

export
endBy : {c : Bool} ->
        (sep : Grammar tok True s) ->
        (p : Grammar tok c a) ->
        Grammar tok False (List a)
endBy sep p = option [] $ endBy1 sep p

||| Parse zero or more instances of `p`, separated and terminated by `sep`,
||| returning the parsed items and a proof that the resulting list is non-empty.
export
endBy1' : {c : Bool} ->
          (sep : Grammar tok True s) ->
          (p : Grammar tok c a) ->
          Grammar tok True (xs : List a ** NonEmpty xs)
endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in
                                    p <* sep

||| Parse an instance of `p` that is between `left` and `right`.
export
between : {c : Bool} ->
          (left : Grammar tok True l) ->
          (right : Grammar tok True r) ->
          (p : Grammar tok c a) ->
          Grammar tok True a
between left right contents = left *> contents <* right


text:
module Rhone.JS

import public Control.Arrow
import public Control.Category
import public Control.Monad.Dom
import public Control.MonadRec
import public Data.MSF
import public JS
import public Rhone.JS.Input
import public Rhone.JS.Sink
import public Rhone.JS.Source
import public Rhone.JS.Util
import public Text.Html as Html
import public Web.Dom