text:
module BezoutsIdentity

import Data.Vect

{-

NOTES

Though the assumptions seem so obvious you shouldn't have to prove them,
either they're wrong together or Idris is very broken, because we've
proven (6 = 2) by proving (a, b)===(0, 1) satisfies a*4+b*6 = gcd 4 6.
I suspect the error is `subtractionexchangepr` and subtraction of Nats
is broken, but it could also be `gcddef`, which shows up in the
expression for the proof of this fact a few times (and shows up
in the correct computations we've seen as well).

Further, the linear combination can't be right, because the only solutions
have negative coefficients in them.

Oh! No, it's clearly modeqpr that's wrong. It assumes (+k).(-k) = id.
But subtractionexchangepr might still be wrong for the same reason.

===========================================

TODO

Prove bezoutsIdentityNat rigorously and over ZZ. Find the contradiction

	> bezoutsIdentityNat 4 6

is false while

	> bezoutsIdentityNat 4 2

is true.

But we CAN'T just do it over ZZ, because `gcd` is not defined for it (what??).
We need to use Int or Integral or (Integral a, Quasigroup a) => a, but be warned
this algorithm will still fail if the number system has Integral instantiated but
it is not either one of those two or a Euclidean domain.

	Prelude.Nat.toIntNat : Nat -> Int
	Tail recursive cast Nat to Int Note that this can overflow

	Prelude.Nat.toIntegerNat : Nat -> Integer
	Convert a Nat to an Integer

So we want to use Integer instead of Int.

	Prelude.Nat.fromIntegerNat : Integer -> Nat
	Convert an Integer to a Nat, mapping negative numbers to 0

We can use this to build a nice `abs`.

Remove gcddef by proving this trivial lemma

Remove junk from lemma_gcdrecpr by inspecting the proof
See if it can't be done in a more uniform style
 style 1a) more letting things be the Refl ComputableThm
 style 1b) more claims of equalities combined combinatorially
 style 2) more functional, creating intermediate assumptions by applying
 	Clearly gluemap is the wrong kind of function.
 	On the other hand, we described how to express the proof maneuvers as plumbing.
 	Maybe we could extend the plumbing to where we don't need some of the proof hints,
 	say by replacing the value whose equal expression needs to be hinted at being
 	wrapped in a function definition with a relative derivation by some other function
 	that rewrite w/ cong will be happy to recognize, such as so factorizing the thm at claim.

Expressions of the plumbing being performed that are more generally are desired

Perhaps we should call what we're proving now the Euclidean division algorithm,
and call the witness-erased form, corresponding to the existential form of the
conclusion, the true Bezout's theorem.
> :apropos Exists

Refactor into modules based on independence of origins.

===========================================

IMPACT OF LANGUAGE GAPS ON CODE

Here's some semantics errors within rewrite, possibly due to misscoping.
This was found in lemma_gcdrecpr, right where ?subtractionexchange is made.

> rewrite sym ( ( the ( (a : Nat) -> (b : Nat) -> (c : Nat) -> (a-b)+c = a+(c-b) ) ?subtractionexchange ) $ ( a*d ) $ ( (b*(div (c-r) d))*d ) $ ( b*c ) )
	Error: Perhaps a is applied to too many arguments
> rewrite sym ( ( the ( (x : Nat) -> (y : Nat) -> (z : Nat) -> (x-y)+z = x+(z-y) ) ?subtractionexchange ) ( a*d ) ( (b*(div (c-r) d))*d ) ( b*c ) )
	Error: No such variable x

Some things can't be made private even though they shouldn't be used outside this module,
because doing so will change how things in this module that use them typecheck, creating
a bug which allows a using function's type to be checked but appears undeclared when called.
This was found by making gcdwzeroproof private and checking the type of bezoutsIdentityNat 1.

Making gcdwzeroproof private also prevents gcdnormally=?gcdnormallyproof from being able to access
all the variables from the environment that are involved.

It would be nice if we knew how to use a proof of equality of types to refine a goal.
Maybe it would use refine.
We need to prove the type of the goal matches what we have,
not that we have a value of the goal type.

Then we could replace (bezeqty c d nn) with
	let (a,b)=nn in a*c+b*d = gcd c d
or	(\(a,b) => a*c+b*d = gcd c d) nn

-}

gcdwzeroproof : (cc : Nat) -> plus (plus cc 0) 0 = cc
gcdwzeroproof = proof
	intro
	rewrite sym (plusCommutative cc 0)
	rewrite sym (plusCommutative cc 0)
	trivial

gcddef : (a : Nat) -> (b : Nat) -> ( gcd a b = assert_total (gcd b (modNat a b)) )
-- Type mismatch on the equality, even though the things are equal by def.
-- gcddef a b = Refl
gcddef a b = believe_me "by definition"

{-

Proof sketch
In this style, some of the arrows are tautological from prior knowledge
If the use of `r` for `modNat c d` til the conclusion were followed,
the actual proof would be easier to follow and more elegantly written.

lemma_gcdrec : (c : Nat) -> (d : Nat) -> (r : Nat) -> (a : Nat) -> (b : Nat)
	-> (r = modNat c d)
	-> (a*d+b*r = gcd d r)
	-> ( gcd d r = gcd c d ) --by def of gcd
	-> ( a*d + b*r = gcd c d ) -- by subst b-n previous two

	-> ( r+(div (c-r) d)d = c ) -- Solution exists by lifting r over multiples of d to c. Namely, d | c-r.
	-> ( r = c-(div (c-r) d)d ) -- by cong on subtraction
	-> ( (a*d + b*(c-(div (c-r) d)*d)) = gcd c d ) -- by subst b-n prev 3
	-> ( ((a-b*(div (c-r) d))*d + b*c) = gcd c d ) -- by distrib then assoc then distrib

-}

lemma_gcdrec : (c : Nat) -> (d : Nat) -> (a : Nat) -> (b : Nat)
	-> ( gcdformknown : a*d+b*(modNat c d) = gcd d (modNat c d))
	-> ( ((a-b*(div (c-(modNat c d)) d))*d + b*c) = gcd c d )
lemma_gcdrec = ?lemma_gcdrecpr

-- A bunch of this is junk. If we try again, we can cut that out.
lemma_gcdrecpr = proof
  intros
  claim lincombformknown ( a*d+b*(modNat c d) = gcd c d )
  unfocus
  claim modeq ( modNat c d = c-(div (c-(modNat c d)) d)*d )
  unfocus
  claim substform ( ((a-b*(div (c-(modNat c d)) d))*d + b*c) = gcd c d )
  unfocus
  rewrite sym ( multDistributesOverMinusLeft a (b*(div (c-(modNat c d)) d)) d )
  claim subtractionexchange (x : Nat) -> (y : Nat) -> (z : Nat) -> plus (minus x y) z = plus x (minus z y)
  unfocus
  rewrite sym ( subtractionexchange (a*d) ( (b*(div (c-(modNat c d)) d))*d ) ( b*c ) )
  rewrite sym (sym $ multAssociative b (div (c-(modNat c d)) d) d)
  rewrite sym (sym $ multDistributesOverMinusRight b c ((div (c-(modNat c d)) d)*d))
  claim substform' ( (a*d + b*(c-(div (c-(modNat c d)) d)*d)) = gcd c d )
  unfocus
  exact substform'
  rewrite sym (gcddef c d)
  exact gcdformknown
  unfocus
  exact (believe_me "Rm this junk")
  exact ?subtractionexchangepr
  rewrite sym (gcddef c d)
  -- rewrite sym (sym modeq) is no-opping, but should solve the main thm
  --    REDO: Maybe we just need to use compute to normalize the goal terms beforehand?
  -- So, we have to add hints, namely factoring through what we call
  -- reachfortheglue and applying cong and trans.
  -- The type of such a maneuver is roughly {a : A} -> {b : A} -> {c : B} -> (a = b) -> { f : A -> B } -> ( f b = c ) -> ( f a = c )
  -- This gluemap map is junk we recreate later.
  claim gluemap ( gf : plus (mult a d) (mult b (modNat c d)) = gcd d (modNat c d) ) -> ( me : modNat c d = c - div (c - modNat c d) d * d ) -> a * d + b * (c - div (c - modNat c d) d * d) = gcd d (modNat c d)
  intros
  let reachfortheglue = \v => plus (mult a d) (mult b v)
  let rftgv = cong {f=reachfortheglue} me
  let fv = the ( reachfortheglue ( c - div (c - modNat c d) d * d ) = plus (mult a d) (mult b $ c - div (c - modNat c d) d * d) ) Refl
  let t_rftgv_fv = trans rftgv fv
  let t_trftgvfg_gf = trans (sym t_rftgv_fv) gf
  exact t_trftgvfg_gf
  let reachfortheglue = \v => plus (mult a d) (mult b v)
  let rftgv = cong {f=reachfortheglue} modeq
  let fv = the ( reachfortheglue ( c - div (c - modNat c d) d * d ) = plus (mult a d) (mult b $ c - div (c - modNat c d) d * d) ) Refl
  let t_rftgv_fv = trans rftgv fv
  let t_trftgvfg_gf = trans (sym t_rftgv_fv) gcdformknown
  exact t_trftgvfg_gf
  exact (?modeqpr c d)

total
bezeqty : Nat -> Nat -> (Nat,Nat) -> Type
bezeqty c d (a,b) = a*c+b*d = gcd c d

lemma_gcdrecdepparout : (c : Nat) -> (d : Nat) -> (a : Nat) -> (b : Nat)
	-> ( gcdformknown : bezeqty d (modNat c d) (a,b))
	-> ( nn:(Nat,Nat) ** bezeqty c d nn )
lemma_gcdrecdepparout = ?lemma_gcdrecdepparoutpr

lemma_gcdrecdepparoutpr = proof
  intros
  claim imedeq ( b*c + (a-b*(div (c-(modNat c d)) d))*d = gcd c d )
  unfocus
  exact ( (b, (a - b * div (c - modNat c d) d)) ** imedeq )
  -- here we see the sum in the conclusion of lemma_gcdrec
  -- differs in term order from that needed
  rewrite sym (sym $ lemma_gcdrec c d a b gcdformknown)
  compute
  rewrite sym ( plusCommutative (mult b c) (mult (minus a (mult b (div (minus c (modNat c d)) d))) d) )
  exact Refl

bezoutsIdentityNat : (c:Nat) -> (d:Nat)
	-> ( nn : (Nat,Nat) ** bezeqty c d nn )
bezoutsIdentityNat c Z = ((1,0) ** gcdwzero)
	where
		gcdwzero = gcdwzeroproof c
bezoutsIdentityNat c d with (bezoutsIdentityNat d (modNat c d))
	| ((a,b) ** oldpr) = lemma_gcdrecdepparout c d a b oldpr


text:
module Bad3

badExpr : ()
badExpr (whatever : ())

ext: idr


text:
module CH11

import Data.Primitives.Views

every_other : Stream Int -> Stream Int
every_other (_ :: x :: xs) = x :: every_other xs

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

implementation Functor InfList where
  -- map : (a -> b) -> InfList a -> InfList b
  map f (value :: inflist) = f value :: map f inflist

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : Nat -> InfList a -> List a
getPrefix Z xs            = []
getPrefix (S k) (x :: xs) = x :: getPrefix k xs

data Face = Head | Tail

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223
               in (seed' `shiftR` 2) :: randoms seed'

getFace : Int -> Face
getFace n with (divides n 2)
  getFace (2 * q + r) | DivBy prf = if r == 0 then Head else Tail

coinFlips : Nat -> Stream Int -> List Face
coinFlips Z xs            = []
coinFlips (S k) (x :: xs) = getFace x :: coinFlips k xs


text:
-- Vector.idr
--
-- Working with vectors and length-constraint lists

import Data.Vect

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

sixInts : Vect 6 Int
sixInts = [4, 5, 6, 7, 8, 9]

tenInts : Vect 10 Int
tenInts = fourInts ++ sixInts

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Idrlisp.Vec

import Data.IOArray

%default total

||| An abstract representation of idrlisp vectors.
export
data Vec a
  = NonEmpty (IOArray a) Int
  | Empty

export
length : Vec a -> Nat
length Empty = 0
length (NonEmpty _ l) = cast l

export
empty : Vec a
empty = Empty

export
new : Nat -> a -> IO (Vec a)
new size zero = do
  array <- newArray (cast size) zero
  pure $ NonEmpty array (cast size)

export
fromList : List a -> IO (Vec a)
fromList [] = pure empty
fromList (x :: xs) = do
  let l : Int = cast (length xs)
  array <- newArray (1 + l) x
  sequence_ $ zipWith (unsafeWriteArray array) [1,2..l] xs
  pure $ NonEmpty array (1 + l)

export
toList : Vec a -> IO (List a)
toList Empty = pure []
toList (NonEmpty arr l) = traverse (unsafeReadArray arr) [0,1..l-1]

export
read : Nat -> Vec a -> IO (Maybe a)
read index Empty = pure Nothing
read index (NonEmpty arr l) =
  if l <= cast index
    then pure Nothing
    else Just <$> unsafeReadArray arr (cast index)

export
write : Nat -> a -> Vec a -> IO Bool
write index value Empty = pure False
write index value (NonEmpty arr l) =
  if l <= cast index
    then pure False
    else unsafeWriteArray arr (cast index) value *> pure True

export
copy : Vec a -> Nat -> Vec a -> Nat -> Nat -> IO Bool
copy src srcStart dest destStart Z =
  pure $ srcStart <= length src && destStart <= length dest
copy (NonEmpty src srcLen) srcStart (NonEmpty dest destLen) destStart (S len) =
  if srcStart + S len <= cast srcLen && destStart + S len <= cast destLen
    then traverse readWrite [0,1..len] *> pure True
    else pure False
  where
    readWrite : Nat -> IO ()
    readWrite i =
      unsafeReadArray src (cast (i + srcStart)) >>=
      unsafeWriteArray dest (cast (i + destStart))
copy src srcStart dest destStart len = pure False

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Test.RnaTranscription

import RnaTranscription
import Data.Vect

%access export

assertCase : Eq b => (a -> b) -> (String, a, b) -> IO ()
assertCase fn (desc,given,expected) = do
  putStrLn desc
  if fn given == expected
     then putStrLn "  Test Passed"
     else putStrLn "  Test Failed"

testCases : List (n : Nat ** (String, Vect n DnaStrand, Vect n RnaStrand))
testCases = [(_ ** ("RNA complement of cytosine is guanine", [C],                       [G])),
             (_ ** ("RNA complement of guanine is cytosine", [G],                       [C])),
             (_ ** ("RNA complement of thymine is adenine",  [T],                       [A])),
             (_ ** ("RNA complement of adenine is uracil",   [A],                       [U])),
             (_ ** ("RNA complement",                        [A,C,G,T,G,G,T,C,T,T,A,A], [U,G,C,A,C,C,A,G,A,A,U,U]))]

runTests : IO ()
runTests = traverse_ testCase' testCases
  where testCase' : (n : Nat ** (String, Vect n DnaStrand, Vect n RnaStrand)) -> IO ()
        testCase' (x ** pf) = assertCase toRna pf


text:
module Sub09LTE18t15

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(3t+2)+3 --C[4,-4]--> 6t+3
export
lte18t15 : (j : Nat) -> LTE (S j) (S (S (plus (plus j j) j)))
lte18t15 Z     = (lteSuccRight . LTESucc) LTEZero
lte18t15 (S j) =
  let lemma = lte18t15 j in
  rewrite (sym (plusSuccRightSucc j j)) in
  rewrite (sym (plusSuccRightSucc (plus j j) j)) in
    (lteSuccRight . lteSuccRight . LTESucc) lemma


text:
module Core.SchemeEval.Compile

{- TODO:

- Make a decent set of test cases
- Option to keep vs discard FCs for faster quoting where we don't need FC

Advanced TODO (possibly not worth it...):
- Write a conversion check
- Extend unification to use SObj; include SObj in Glued

-}

import Core.Case.CaseTree
import Core.Context
import Core.Core
import Core.Directory
import Core.SchemeEval.Builtins
import Core.SchemeEval.ToScheme
import Core.TT

import Data.List

import Libraries.Utils.Scheme
import System.Info

schString : String -> String
schString s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar c = if isAlphaNum c || c =='_'
                  then cast c
                  else "C-" ++ show (cast {to=Int} c)

schVarUN : UserName -> String
schVarUN (Basic n) = schString n
schVarUN (Field n) = "rf--" ++ schString n
schVarUN Underscore = "_US_"

schVarName : Name -> String
schVarName (NS ns (UN n))
   = schString (showNSWithSep "-" ns) ++ "-" ++ schVarUN n
schVarName (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schVarName n
schVarName (UN n) = "u--" ++ schVarUN n
schVarName (MN n i) = schString n ++ "-" ++ show i
schVarName (PV n d) = "pat--" ++ schVarName n
schVarName (DN _ n) = schVarName n
schVarName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schVarName n
schVarName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
schVarName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y
schVarName (Resolved i) = "fn--" ++ show i

schName : Name -> String
schName n = "ct-" ++ schVarName n

export
data Sym : Type where

export
nextName : Ref Sym Integer => Core Integer
nextName
    = do n <- get Sym
         put Sym (n + 1)
         pure n

public export
data SVar = Bound String | Free String

Show SVar where
  show (Bound x) = x
  show (Free x) = "'" ++ x

export
getName : SVar -> String
getName (Bound x) = x
getName (Free x) = x

public export
data SchVars : List Name -> Type where
     Nil : SchVars []
     (::) : SVar -> SchVars ns -> SchVars (n :: ns)

Show (SchVars ns) where
  show xs = show (toList xs)
    where
      toList : forall ns . SchVars ns -> List String
      toList [] = []
      toList (Bound x :: xs) = x :: toList xs
      toList (Free x :: xs) = "'x" :: toList xs

getSchVar : {idx : _} -> (0 _ : IsVar n idx vars) -> SchVars vars -> String
getSchVar First (Bound x :: xs) = x
getSchVar First (Free x :: xs) = "'" ++ x
getSchVar (Later p) (x :: xs) = getSchVar p xs

{-

Encoding of NF -> Scheme

Maybe consider putting this back into a logical order, rather than the order
I implemented them in...

vector (tag>=0) name args == data constructor
vector (-10) (name, arity) (args as list) == blocked meta application
                   (needs to be same arity as block app, for ct-addArg)
vector (-11) symbol (args as list) == blocked local application
vector (-1) ... == type constructor
vector (-2) name (args as list) == blocked application
vector (-3) ... == Pi binder
vector (-4) ... == delay arg
vector (-5) ... == force arg
vector (-6) = Erased
vector (-7) = Type
vector (-8) ... = Lambda
vector (-9) blockedapp proc = Top level lambda (from a PMDef, so not expanded)
vector (-12) ... = PVar binding
vector (-13) ... = PVTy binding
vector (-14) ... = PLet binding
vector (-15) ... = Delayed

vector (-100 onwards) ... = constants
-}

blockedAppWith : Name -> List (SchemeObj Write) -> SchemeObj Write
blockedAppWith n args = Vector (-2) [toScheme n, vars args]
  where
    vars : List (SchemeObj Write) -> SchemeObj Write
    vars [] = Null
    vars (x :: xs) = Cons x (vars xs)

blockedMetaApp : Name -> SchemeObj Write
blockedMetaApp n
    = Lambda ["arity-0"] (Vector (-10) [Cons (toScheme n) (Var "arity-0"),
                                        Null])

unload : SchemeObj Write -> List (SchemeObj Write) -> SchemeObj Write
unload f [] = f
unload f (a :: as) = unload (Apply (Var "ct-app") [f, a]) as

compileConstant : FC -> Constant -> SchemeObj Write
compileConstant fc (I x) = Vector (-100) [IntegerVal (cast x)]
compileConstant fc (I8 x) = Vector (-101) [IntegerVal (cast x)]
compileConstant fc (I16 x) = Vector (-102) [IntegerVal (cast x)]
compileConstant fc (I32 x) = Vector (-103) [IntegerVal (cast x)]
compileConstant fc (I64 x) = Vector (-104) [IntegerVal (cast x)]
compileConstant fc (BI x) = Vector (-105) [IntegerVal x]
compileConstant fc (B8 x) = Vector (-106) [IntegerVal (cast x)]
compileConstant fc (B16 x) = Vector (-107) [IntegerVal (cast x)]
compileConstant fc (B32 x) = Vector (-108) [IntegerVal (cast x)]
compileConstant fc (B64 x) = Vector (-109) [IntegerVal (cast x)]
compileConstant fc (Str x) = StringVal x
compileConstant fc (Ch x) = CharVal x
compileConstant fc (Db x) = FloatVal x
-- Constant types get compiled as TyCon names, for matching purposes
compileConstant fc t
    = Vector (-1) [IntegerVal (cast (constTag t)),
                   StringVal (show t),
                   toScheme (UN (Basic (show t))),
                   toScheme fc]

compileStk : Ref Sym Integer =>
             {auto c : Ref Ctxt Defs} ->
             SchVars vars -> List (SchemeObj Write) -> Term vars ->
             Core (SchemeObj Write)

compilePiInfo : Ref Sym Integer =>
                {auto c : Ref Ctxt Defs} ->
                SchVars vars -> PiInfo (Term vars) ->
                Core (PiInfo (SchemeObj Write))
compilePiInfo svs Implicit = pure Implicit
compilePiInfo svs Explicit = pure Explicit
compilePiInfo svs AutoImplicit = pure AutoImplicit
compilePiInfo svs (DefImplicit t)
    = do t' <- compileStk svs [] t
         pure (DefImplicit t')

compileStk svs stk (Local fc isLet idx p)
    = pure $ unload (Var (getSchVar p svs)) stk
-- We are assuming that the bound name is a valid scheme symbol. We should
-- only see this when inventing temporary names during quoting
compileStk svs stk (Ref fc Bound name)
    = pure $ unload (Symbol (show name)) stk
compileStk svs stk (Ref fc (DataCon t a) name)
    = if length stk == a -- inline it if it's fully applied
         then pure $ Vector (cast t)
                       (toScheme !(toResolvedNames name) ::
                        toScheme fc :: stk)
         else pure $ unload (Apply (Var (schName name)) []) stk
compileStk svs stk (Ref fc (TyCon t a) name)
    = if length stk == a -- inline it if it's fully applied
         then pure $ Vector (-1)
                       (IntegerVal (cast t) ::
                        StringVal (show name) ::
                        toScheme !(toResolvedNames name) ::
                        toScheme fc :: stk)
         else pure $ unload (Apply (Var (schName name)) []) stk
compileStk svs stk (Ref fc x name)
    = pure $ unload (Apply (Var (schName name)) []) stk
compileStk svs stk (Meta fc name i xs)
    = do xs' <- traverse (compileStk svs stk) xs
         -- we encode the arity as first argument to the hole definition, which
         -- helps in readback, so we have to apply the hole function to the
         -- length of xs to be able to restore the Meta properly
         pure $ unload (Apply (Var (schName name)) [])
                       (IntegerVal (cast (length xs)) :: stk ++ xs')
compileStk svs stk (Bind fc x (Let _ _ val _) scope)
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         val' <- compileStk svs [] val
         sc' <- compileStk (Bound x' :: svs) [] scope
         pure $ unload (Let x' val' sc') stk
compileStk svs stk (Bind fc x (Pi _ rig p ty) scope)
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         ty' <- compileStk svs [] ty
         sc' <- compileStk (Bound x' :: svs) [] scope
         p' <- compilePiInfo svs p
         pure $ Vector (-3) [Lambda [x'] sc', toScheme rig, toSchemePi p',
                                              ty', toScheme x]
compileStk svs stk (Bind fc x (PVar _ rig p ty) scope)
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         ty' <- compileStk svs [] ty
         sc' <- compileStk (Bound x' :: svs) [] scope
         p' <- compilePiInfo svs p
         pure $ Vector (-12) [Lambda [x'] sc', toScheme rig, toSchemePi p',
                                               ty', toScheme x]
compileStk svs stk (Bind fc x (PVTy _ rig ty) scope)
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         ty' <- compileStk svs [] ty
         sc' <- compileStk (Bound x' :: svs) [] scope
         pure $ Vector (-13) [Lambda [x'] sc', toScheme rig, ty', toScheme x]
compileStk svs stk (Bind fc x (PLet _ rig val ty) scope) -- we only see this on LHS
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         val' <- compileStk svs [] val
         ty' <- compileStk svs [] ty
         sc' <- compileStk (Bound x' :: svs) [] scope
         pure $ Vector (-14) [Lambda [x'] sc', toScheme rig, val', ty', toScheme x]
compileStk svs [] (Bind fc x (Lam _ rig p ty) scope)
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         ty' <- compileStk svs [] ty
         sc' <- compileStk (Bound x' :: svs) [] scope
         p' <- compilePiInfo svs p
         pure $ Vector (-8) [Lambda [x'] sc', toScheme rig, toSchemePi p',
                                              ty', toScheme x]
compileStk svs (s :: stk) (Bind fc x (Lam _ _ _ _) scope)
    = do i <- nextName
         let x' = schVarName x ++ "-" ++ show i
         sc' <- compileStk (Bound x' :: svs) stk scope
         pure $ Apply (Lambda [x'] sc') [s]
compileStk svs stk (App fc fn arg)
    = compileStk svs (!(compileStk svs [] arg) :: stk) fn
-- We're only using this evaluator for REPL and typechecking, not for
-- tidying up definitions or LHSs, so we'll always remove As patterns
compileStk svs stk (As fc x as pat) = compileStk svs stk pat
compileStk svs stk (TDelayed fc r ty)
    = do ty' <- compileStk svs stk ty
         pure $ Vector (-15) [toScheme r, ty']
compileStk svs stk (TDelay fc r ty arg)
    = do ty' <- compileStk svs [] ty
         arg' <- compileStk svs [] arg
         pure $ Vector (-4) [toScheme r, toScheme fc,
                             Lambda [] ty', Lambda [] arg']
compileStk svs stk (TForce fc x tm)
    = do tm' <- compileStk svs [] tm
         pure $ Apply (Var "ct-doForce")
                      [tm',
                      Vector (-5) [toScheme x, toScheme fc, Lambda [] tm']]
compileStk svs stk (PrimVal fc c) = pure $ compileConstant fc c
compileStk svs stk (Erased fc imp) = pure $ Vector (-6) [toScheme fc, toScheme imp]
compileStk svs stk (TType fc u) = pure $ Vector (-7) [toScheme fc, toScheme u]

export
compile : Ref Sym Integer =>
          {auto c : Ref Ctxt Defs} ->
          SchVars vars -> Term vars -> Core (SchemeObj Write)
compile vars tm = compileStk vars [] tm

getArgName : Ref Sym Integer =>
             Core Name
getArgName
    = do i <- nextName
         pure (MN "carg" (cast i))

extend : Ref Sym Integer =>
         (args : List Name) -> SchVars vars ->
         Core (List Name, SchVars (args ++ vars))
extend [] svs = pure ([], svs)
extend (arg :: args) svs
    = do n <- getArgName
         (args', svs') <- extend args svs
         pure (n :: args', Bound (schVarName n) :: svs')

compileCase : Ref Sym Integer =>
              {auto c : Ref Ctxt Defs} ->
              (blocked : SchemeObj Write) ->
              SchVars vars -> CaseTree vars -> Core (SchemeObj Write)
compileCase blk svs (Case idx p scTy xs)
    = case !(caseType xs) of
           CON => toSchemeConCases idx p xs
           TYCON => toSchemeTyConCases idx p xs
           DELAY => toSchemeDelayCases idx p xs
           CONST => toSchemeConstCases idx p xs
  where
    data CaseType = CON | TYCON | DELAY | CONST

    caseType : List (CaseAlt vs) -> Core CaseType
    caseType [] = pure CON
    caseType (ConCase x tag args y :: xs)
        = do defs <- get Ctxt
             Just gdef <- lookupCtxtExact x (gamma defs)
                  | Nothing => pure TYCON -- primitive type match
             case definition gdef of
                  DCon{} => pure CON
                  TCon{} => pure TYCON
                  _ => pure CON -- or maybe throw?
    caseType (DelayCase ty arg x :: xs) = pure DELAY
    caseType (ConstCase x y :: xs) = pure CONST
    caseType (DefaultCase x :: xs) = caseType xs

    makeDefault : List (CaseAlt vars) -> Core (SchemeObj Write)
    makeDefault [] = pure blk
    makeDefault (DefaultCase sc :: xs) = compileCase blk svs sc
    makeDefault (_ :: xs) = makeDefault xs

    toSchemeConCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
                       List (CaseAlt vars) -> Core (SchemeObj Write)
    toSchemeConCases idx p alts
        = do let var = getSchVar p svs
             alts' <- traverse (makeAlt var) alts
             let caseblock
                    = Case (Apply (Var "vector-ref") [Var var, IntegerVal 0])
                           (mapMaybe id alts')
                           (Just !(makeDefault alts))
             pure $ If (Apply (Var "ct-isDataCon") [Var var])
                       caseblock
                       blk
      where
        project : Int -> String -> List Name ->
                  SchemeObj Write -> SchemeObj Write
        project i var [] body = body
        project i var (n :: ns) body
            = Let (schVarName n)
                  (Apply (Var "vector-ref") [Var var, IntegerVal (cast i)])
                  (project (i + 1) var ns body)

        bindArgs : String -> (args : List Name) -> CaseTree (args ++ vars) ->
                   Core (SchemeObj Write)
        bindArgs var args sc
            = do (bind, svs') <- extend args svs
                 project 3 var bind <$> compileCase blk svs' sc

        makeAlt : String -> CaseAlt vars ->
                  Core (Maybe (SchemeObj Write, SchemeObj Write))
        makeAlt var (ConCase n t args sc)
            = pure $ Just (IntegerVal (cast t), !(bindArgs var args sc))
        -- TODO: Matching on types, including ->
        makeAlt var _ = pure Nothing

    toSchemeTyConCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
                         List (CaseAlt vars) -> Core (SchemeObj Write)
    toSchemeTyConCases idx p alts
        = do let var = getSchVar p svs
             alts' <- traverse (makeAlt var) alts
             caseblock <- addPiMatch var alts
                      -- work on the name, so the 2nd arg
                            (Case (Apply (Var "vector-ref") [Var var, IntegerVal 2])
                               (mapMaybe id alts')
                               (Just !(makeDefault alts)))
             pure $ If (Apply (Var "ct-isTypeMatchable") [Var var])
                       caseblock
                       blk
      where
        project : Int -> String -> List Name ->
                  SchemeObj Write -> SchemeObj Write
        project i var [] body = body
        project i var (n :: ns) body
            = Let (schVarName n)
                  (Apply (Var "vector-ref") [Var var, IntegerVal (cast i)])
                  (project (i + 1) var ns body)

        bindArgs : String -> (args : List Name) -> CaseTree (args ++ vars) ->
                   Core (SchemeObj Write)
        bindArgs var args sc
            = do (bind, svs') <- extend args svs
                 project 5 var bind <$> compileCase blk svs' sc

        makeAlt : String -> CaseAlt vars ->
                  Core (Maybe (SchemeObj Write, SchemeObj Write))
        makeAlt var (ConCase (UN (Basic "->")) t [_, _] sc)
            = pure Nothing -- do this in 'addPiMatch' below, since the
                           -- representation is different
        makeAlt var (ConCase n t args sc)
            = pure $ Just (StringVal (show n), !(bindArgs var args sc))
        makeAlt var _ = pure Nothing

        addPiMatch : String -> List (CaseAlt vars) -> SchemeObj Write ->
                     Core (SchemeObj Write)
        addPiMatch var [] def = pure def
        -- t is a function type, and conveniently the scope of a pi
        -- binding is represented as a function. Lucky us! So we just need
        -- to extract it then evaluate the scope
        addPiMatch var (ConCase (UN (Basic "->")) _ [s, t] sc :: _) def
            = do sn <- getArgName
                 tn <- getArgName
                 let svs' = Bound (schVarName sn) ::
                              Bound (schVarName tn) :: svs
                 sc' <- compileCase blk svs' sc
                 pure $ If (Apply (Var "ct-isPi") [Var var])
                           (Let (schVarName sn) (Apply (Var "vector-ref") [Var var, IntegerVal 4]) $
                            Let (schVarName tn) (Apply (Var "vector-ref") [Var var, IntegerVal 1]) $
                            sc')
                           def
        addPiMatch var (x :: xs) def = addPiMatch var xs def

    toSchemeConstCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
                         List (CaseAlt vars) -> Core (SchemeObj Write)
    toSchemeConstCases x p alts
        = do let var = getSchVar p svs
             alts' <- traverse (makeAlt var) alts
             let caseblock
                    = Cond (mapMaybe id alts')
                           (Just !(makeDefault alts))
             pure $ If (Apply (Var "ct-isConstant") [Var var])
                       caseblock
                       blk
     where
        makeAlt : String -> CaseAlt vars ->
                  Core (Maybe (SchemeObj Write, SchemeObj Write))
        makeAlt var (ConstCase c sc)
            = do sc' <- compileCase blk svs sc
                 pure (Just (Apply (Var "equal?")
                               [Var var, compileConstant emptyFC c], sc'))
        makeAlt var _ = pure Nothing

    toSchemeDelayCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
                         List (CaseAlt vars) -> Core (SchemeObj Write)
    -- there will only ever be one, or a default case
    toSchemeDelayCases idx p (DelayCase ty arg sc :: rest)
        = do let var = getSchVar p svs
             tyn <- getArgName
             argn <- getArgName
             let svs' = Bound (schVarName tyn) ::
                          Bound (schVarName argn) :: svs
             sc' <- compileCase blk svs' sc
             pure $ If (Apply (Var "ct-isDelay") [Var var])
                       (Let (schVarName tyn)
                           (Apply (Apply (Var "vector-ref") [Var var, IntegerVal 3]) []) $
                        Let (schVarName argn)
                           (Apply (Apply (Var "vector-ref") [Var var, IntegerVal 4]) []) $
                         sc')
                       blk
    toSchemeDelayCases idx p (_ :: rest) = toSchemeDelayCases idx p rest
    toSchemeDelayCases idx p _ = pure Null

compileCase blk vars (STerm _ tm) = compile vars tm
compileCase blk vars _ = pure blk

varObjs : SchVars ns -> List (SchemeObj Write)
varObjs [] = []
varObjs (x :: xs) = Var (show x) :: varObjs xs

mkArgs : (ns : List Name) -> Core (SchVars ns)
mkArgs [] = pure []
mkArgs (x :: xs)
    = pure $ Bound (schVarName x) :: !(mkArgs xs)

bindArgs : Name ->
           (todo : SchVars ns) ->
           (done : List (SchemeObj Write)) ->
           SchemeObj Write -> SchemeObj Write
bindArgs n [] done body = body
bindArgs n (x :: xs) done body
    = Vector (-9) [blockedAppWith n (reverse done),
                   Lambda [show x]
                      (bindArgs n xs (Var (show x) :: done) body)]

compileBody : {auto c : Ref Ctxt Defs} ->
              Bool -> -- okay to reduce (if False, block)
              Name -> Def -> Core (SchemeObj Write)
compileBody _ n None = pure $ blockedAppWith n []
compileBody redok n (PMDef pminfo args treeCT treeRT pats)
    = do i <- newRef Sym 0
         argvs <- mkArgs args
         let blk = blockedAppWith n (varObjs argvs)
         body <- compileCase blk argvs treeCT
         let body' = if redok
                        then If (Apply (Var "ct-isBlockAll") []) blk body
                        else blk
         -- If it arose from a hole, we need to take an extra argument for
         -- the arity since that's what Meta gets applied to
         case holeInfo pminfo of
              NotHole => pure (bindArgs n argvs [] body')
              SolvedHole _ => pure (Lambda ["h-0"] (bindArgs n argvs [] body'))
compileBody _ n (ExternDef arity) = pure $ blockedAppWith n []
compileBody _ n (ForeignDef arity xs) = pure $ blockedAppWith n []
compileBody _ n (Builtin x) = pure $ compileBuiltin n x
compileBody _ n (DCon tag Z newtypeArg)
    = pure $ Vector (cast tag) [toScheme !(toResolvedNames n), toScheme emptyFC]
compileBody _ n (DCon tag arity newtypeArg)
    = do let args = mkArgNs 0 arity
         argvs <- mkArgs args
         let body
               = Vector (cast tag)
                        (toScheme n :: toScheme emptyFC ::
                             map (Var . schVarName) args)
         pure (bindArgs n argvs [] body)
  where
    mkArgNs : Int -> Nat -> List Name
    mkArgNs i Z = []
    mkArgNs i (S k) = MN "arg" i :: mkArgNs (i+1) k
compileBody _ n (TCon tag Z parampos detpos flags mutwith datacons detagabbleBy)
    = pure $ Vector (-1) [IntegerVal (cast tag), StringVal (show n),
                          toScheme n, toScheme emptyFC]
compileBody _ n (TCon tag arity parampos detpos flags mutwith datacons detagabbleBy)
    = do let args = mkArgNs 0 arity
         argvs <- mkArgs args
         let body
               = Vector (-1)
                        (IntegerVal (cast tag) ::
                         StringVal (show n) ::
                          toScheme n :: toScheme emptyFC ::
                            map (Var . schVarName) args)
         pure (bindArgs n argvs [] body)
  where
    mkArgNs : Int -> Nat -> List Name
    mkArgNs i Z = []
    mkArgNs i (S k) = MN "arg" i :: mkArgNs (i+1) k
compileBody _ n (Hole numlocs x) = pure $ blockedMetaApp n
compileBody _ n (BySearch x maxdepth defining) = pure $ blockedMetaApp n
compileBody _ n (Guess guess envbind constraints) = pure $ blockedMetaApp n
compileBody _ n ImpBind = pure $ blockedMetaApp n
compileBody _ n (UniverseLevel _) = pure $ blockedMetaApp n
compileBody _ n Delayed = pure $ blockedMetaApp n

export
compileDef : {auto c : Ref Ctxt Defs} -> SchemeMode -> Name -> Core ()
compileDef mode n_in
    = do n <- toFullNames n_in -- this is handy for readability of generated names
                     -- we used resolved names for blocked names, though, as
                     -- that's a bit better for performance
         defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
              | Nothing => throw (UndefinedName emptyFC n)

         let True = case schemeExpr def of
                         Nothing => True
                         Just (cmode, def) => cmode /= mode
               | _ => pure () -- already done
         -- If we're in BlockExport mode, check whether the name is
         -- available for reduction.
         let redok = mode == EvalAll ||
                       reducibleInAny (currentNS defs :: nestedNS defs)
                                      (fullname def)
                                      (visibility def)
         -- 'n' is used in compileBody for generating names for readback,
         -- and reading back resolved names is quicker because it's just
         -- an integer
         b <- compileBody redok !(toResolvedNames n) !(toFullNames (definition def))
         let schdef = Define (schName n) b

         -- Add the new definition to the current scheme runtime
         Just obj <- coreLift $ evalSchemeObj schdef
              | Nothing => throw (InternalError ("Compiling " ++ show n ++ " failed"))

         -- Record that this one is done
         ignore $ addDef n ({ schemeExpr := Just (mode, schdef) } def)

initEvalWith : {auto c : Ref Ctxt Defs} ->
               String -> Core Bool
initEvalWith "chez"
    = do defs <- get Ctxt
         if defs.schemeEvalLoaded
            then pure True
            else
             catch (do f <- readDataFile "chez/ct-support.ss"
                       Just _ <- coreLift $ evalSchemeStr $ "(begin " ++ f ++ ")"
                            | Nothing => pure False
                       put Ctxt ({ schemeEvalLoaded := True } defs)
                       pure True)
                (\err => pure False)
initEvalWith "racket"
    = do defs <- get Ctxt
         if defs.schemeEvalLoaded
            then pure True
            else
             catch (do f <- readDataFile "racket/ct-support.rkt"
                       Just _ <- coreLift $ evalSchemeStr $ "(begin " ++ f ++ ")"
                            | Nothing => pure False
                       put Ctxt ({ schemeEvalLoaded := True } defs)
                       pure True)
                (\err => do coreLift $ printLn err
                            pure False)
initEvalWith _ = pure False -- only works on Chez for now

-- Initialise the internal functions we need to build/extend blocked
-- applications
-- These are in a support file, chez/support.ss. Returns True if loading
-- and processing succeeds. If it fails, which it probably will during a
-- bootstrap build at least, we can fall back to the default evaluator.
export
initialiseSchemeEval : {auto c : Ref Ctxt Defs} ->
                       Core Bool
initialiseSchemeEval = initEvalWith codegen


text:
> module Finite.Properties

> import Data.Fin
> import Data.Vect
> import Data.Vect.Quantifiers
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Decidable.Predicates
> import Fin.Operations
> import Fin.Properties
> import Vect.Properties
> -- import Isomorphism.Operations
> import Isomorphism.Properties
> import Nat.LTProperties
> import Basic.Operations
> import Fun.Properties
> import Sigma.Sigma
> import Pairs.Operations
> import Tuple.Properties

> %default total

> %access public export

* |Fin n| is finite

> finiteFin : {n : Nat} -> Finite (Fin n)
> finiteFin {n} = MkSigma n isoRefl

* Representations of finite types

> -- toVectComplete : {A : Type} -> (f : Fin n -> A) -> (k : Fin n) -> Elem (f k) (toVect f)

> ||| |toVect| representations of finite types are complete
> toVectComplete : {A : Type} -> (fA : Finite A) -> (a : A) -> Elem a (toVect fA)
> toVectComplete (MkSigma _ iso) a = s3 where
>   s1  :  Elem (from iso (to iso a)) (toVect (from iso))
>   s1  =  toVectComplete (from iso) (to iso a)
>   s2  :  from iso (to iso a) = a
>   s2  =  fromTo iso a
>   s3  :  Elem a (toVect (from iso))
>   s3  =  replace {P = \ z => Elem z (toVect (from iso))} s2 s1
> {-
> toVectComplete fA a = s3 where
>   s1  :  Elem (fromFin fA (toFin fA a)) (toVect fA)
>   s1  =  FinProperties.toVectComplete (fromFin fA) (toFin fA a)
>   s2  :  fromFin fA (toFin fA a) = a
>   s2  =  FromFinToFin fA a
>   s3  :  Elem a (toVect fA)
>   s3  =  replace {P = \ z => Elem z (toVect fA)} s2 s1
> -}
> %freeze toVectComplete -- frozen

> ||| |toVect| representations of finite types are injective
> toVectInjective1 : {A : Type} -> (fA : Finite A) -> Injective1 (toVect fA)
> toVectInjective1 {A} (MkSigma _ iso) i j p = s3 where
>   s1 : index i (toVect (from iso)) = index j (toVect (from iso))
>   s1 = p
>   s2 : (from iso) i = (from iso) j
>   s2 = replace2 {a = A} {a1 = index i (toVect (from iso))} {a2 = (from iso) i}
>                 {b = A} {b1 = index j (toVect (from iso))} {b2 = (from iso) j}
>                 {P = \ a => \b => a = b}
>                 (toVectRepr (from iso) i) (toVectRepr (from iso) j) s1
>   s3 : i = j
>   s3 = injectiveFrom iso i j s2
> %freeze toVectInjective1 -- frozen

* Non empty finite types

> |||
> cardNotZLemma : {A : Type} -> (fA : Finite A) -> A -> CardNotZ fA
> cardNotZLemma fA a = gtZisnotZ (elemLemma {n = card fA} a (toVect fA) (toVectComplete fA a))
> %freeze cardNotZLemma -- frozen

We want to show that, for a finite type |A| and a decidable predicate |P
: A -> Type|, |Exists P| is decidable

< finiteDecLemma : {A : Type} -> {P : A -> Type} -> Finite A -> Dec1 P -> Dec (Exists P)

(See also |finiteDecLemma2| which is a proof without using vectors.)

It is useful to recall (see "VectProperties.lidr") that

< decAny         : {A : Type} -> {P : A -> Type} -> Dec1 P -> Dec1 (Any P)
< AnyExistsLemma : {A : Type} -> {P : A -> Type} -> Any P as -> Exists P
< ElemAnyLemma   : {A : Type} -> {P : A -> Type} -> P a -> Elem a as -> Any P as

With these premises, proving |finiteDecLemma| is almost straightforward:

> finiteDecLemma : {A : Type} -> {P : A -> Type} -> Finite A -> Dec1 P -> Dec (Exists P)
> finiteDecLemma fA dP with (decAny dP (toVect fA))
>   | (Yes prf)   = Yes (AnyExistsLemma prf)
>   | (No contra) = No (\ e => contra (ElemAnyLemma (getProof e) (toVectComplete fA (getWitness e))))
> %freeze finiteDecLemma -- frozen

We pattern match on |decAny dP (toVect fA)|: the result is either a |prf
: Any P (toVect fA)| or a function |contra : Any P (toVect fA) ->
Void|. In the first case we just apply |AnyExistsLemma| to |prf|. This
gives us a value of type |Exists P| which is what we need. In the second
case we have to implement a function of type |Exists P -> Void|. We do
this by applying |contra|. To this end, we need a value of type |Any P
(toVect fA)|. We compute a value of type |Any P (toVect fA)| by applying
|ElemAnyLemma|.

> finiteDecSigmaLemma : {A : Type} -> {P : A -> Type} -> Finite A -> ((a : A) -> Dec (P a)) -> Dec (Sigma A P)
> finiteDecSigmaLemma fA dP with (decAny dP (toVect fA))
>   | (Yes prf)   = Yes (AnySigmaLemma prf)
>   | (No contra) = No (\ e => contra (ElemAnyLemma (getProof e) (toVectComplete fA (getWitness e))))

* Finiteness of products

> ||| If |P| and |Q| are finite, |(P , Q)| is finite
> finiteProduct : {A, B : Type} -> Finite A -> Finite B -> Finite (A, B)
> -- finiteProduct {A} {B} (Evidence m isoA) (Evidence n isoB) =
> --   Evidence (m * n) (isoTrans (pairCong isoA isoB) finPairTimes)
> finiteProduct {A} {B} (MkSigma _ isoA) (MkSigma _ isoB) =
>   MkSigma _ (isoTrans (pairCong isoA isoB) finPairTimes)
> %freeze finiteProduct -- frozen

> finitePair : {A, B : Type} -> Finite A -> Finite B -> Finite (A, B)
> finitePair = finiteProduct
> %freeze finitePair -- frozen

> ||| Tuples of 3 finite types are finite
> finiteTuple3 : {A, B, C : Type} ->
>                Finite A -> Finite B -> Finite C ->
>                Finite (A, B, C)
> finiteTuple3 {A} {B} {C} fA fB fC =
>   MkSigma _ (isoTrans (tuplePairIso3 {A} {B} {C}) (getProof fABC)) where
>     fAB  : Finite (A, B)
>     fAB  = finiteProduct fA fB
>     fABC : Finite ((A, B), C)
>     fABC = finiteProduct fAB fC

> ||| ||| Tuples of 4 finite types are finite
> finiteTuple4 : {A, B, C, D : Type} ->
>                Finite A -> Finite B -> Finite C ->  Finite D ->
>                Finite (A, B, C, D)
> finiteTuple4 {A} {B} {C} {D} fA fB fC fD =
>   MkSigma _ (isoTrans (tuplePairIso4 {A} {B} {C} {D}) (getProof fABCD)) where
>     fABC  : Finite (A, B, C)
>     fABC  = finiteTuple3 fA fB fC
>     fABCD : Finite ((A, B, C), D)
>     fABCD = finiteProduct fABC fD

> {- we have to comply with the new |record| syntax for this to type check

----

Porting the proof from the Vect world to the Finite world.

Pseudo-code: case on the size |n| of the finite set
0: empty set => No
(n+1): case P (A 0) of
         Yes -> Yes
         No  -> recursive call with slightly smaller Finite

Some helpers needed to map between Dec's etc.
In fact, Iso is not needed - we can map already with just any pair of functions:

> decIso' : {X : Type} -> {Y : Type} -> (to : X -> Y) -> (from : Y -> X) -> Dec X -> Dec Y
> decIso' to from (Yes x) = Yes (to x)
> decIso' to from (No nx) = No (nx . from)

> decIso : {X : Type} -> {Y : Type} -> Iso X Y -> Dec X -> Dec Y
> decIso (MkIso to from _ _) = decIso' to from

This |lemma| is roughly where we want to end up:

< lemma : (n : Nat) -> {A : Type} -> FiniteN n A -> {P : A -> Type} -> Dec1 P -> Dec (Exists P)

But let's start with a simpler version, ignoring A for now:

< decExistsFin : (n : Nat) -> (P : Fin n -> Type) -> (dP : Dec1 P) -> Dec (Exists P)

Dec (Exists P) is either Yes (an index (i : Fin n) and a proof (p : P
i)) or No (a function showing that any such "index+proof-pair" is
absurd). To show that, we compute the lowest index for which we get a
Yes, or No if no such index exists.

A predicate over |Fin n| can be seen as a vector, so we use the
helper function |tail| from FinOperations.lidr:

< tail : {A : Type} -> (Fin (S n) -> A) -> (Fin n -> A)
< tail P = P . FS

Similarly |Dec1| over |Fin n| can be seen as a vector of decidability
tests. Thus we also need a |Dec1|-version of tail:

> tailDec1 : {n : Nat} -> {P : Fin (S n) -> Type} -> Dec1 P -> Dec1 (tail P)
> tailDec1 dP = \x => dP (FS x)

REMARK{Nicola}{"tail restrictions of decidable predicates are
decidable". This should hold for no matter what restriction, in
fact. But we do not have a notion of subtype already and therefore we do
not have a notion of restriction.}

Next we define the base- and step-case for decidability of predicates
over |Fin n|:

> decNil : {P : Fin 0 -> Type} -> Dec (Exists P)
> decNil = No (\(Evidence wit pro)=> FinZElim wit)

We defined |decCons| to combine decidability tests for the "head" and
the "tail" of a predicate |P| into decidability for the full
predicate. (Pick the lowest index with a |Yes|.)

> using (n : Nat, P : Fin (S n) -> Type)
>   exiCons  :                    Exists (tail P)  ->      Exists P
>   exiCons (Evidence i p) = Evidence (FS i) p

>   nExiCons : Not (P FZ) -> Not (Exists (tail P)) -> Not (Exists P)
>   nExiCons n0 nt (Evidence FZ      p) = n0 p
>   nExiCons n0 nt (Evidence (FS i)  p) = nt (Evidence i p)

>   decCons  : Dec (P FZ) -> Dec (Exists (tail P)) -> Dec (Exists P)
>   decCons (Yes p) _        = Yes (Evidence FZ p)
>   decCons (No np) (Yes pt) = Yes (exiCons pt)
>   decCons (No np) (No npt) = No  (nExiCons np npt)

Find the lowest index for which |dP| says |Yes|.

> decExistsFin : (n : Nat) -> (P : Fin n -> Type) -> Dec1 P -> Dec (Exists P)
> decExistsFin Z     P dP = decNil
> decExistsFin (S n) P dP = decCons (dP FZ) (decExistsFin n (tail P)
>                                                           (tailDec1 dP))

With the simpler case out of the way we can return to the more general case:

> existsIsoTo : {X : Type} -> {Y : Type} ->
>             (iso : Iso X Y) -> (P : X -> Type) ->
>             Exists (P . (from iso)) -> Exists P
> existsIsoTo {X} {Y} iso P (Evidence y pf) = Evidence (from iso y) pf

> existsIsoFrom : {X : Type} -> {Y : Type} ->
>             (iso : Iso X Y) -> (P : X -> Type) ->
>             Exists P -> Exists (P . (from iso))
> existsIsoFrom {X} {Y} iso P (Evidence x pf) = Evidence (to iso x) pf'
>   where
>     pf' : P (from iso (to iso x))
>     pf' = replace (sym (fromTo iso x)) pf

This is the core result:

> finiteDecHelper : (n : Nat) -> {A : Type} -> FiniteN n A ->
>                   (P : A -> Type) -> Dec1 P -> Dec (Exists P)
> finiteDecHelper n iso P dP = decIso' (existsIsoTo   iso P)
>                                      (existsIsoFrom iso P)
>                                      (decExistsFin n  (P . (from iso))
>                                                       (\x => dP (from iso x)))

which can be packaged up as what we aimed for at the beginning:

> finiteDecLemma2 : {A : Type} -> {P : A -> Type} ->
>                   Finitea2 {P} (Evidence n iso) dP = finiteDecHelper n iso P dP

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| Checking a %builtin pragma is correct.
-- If we get more builtins it might be wise to move each builtin to it's own file.
module TTImp.ProcessBuiltin

import Data.List

import Libraries.Data.Fin as Libs
import Libraries.Data.NameMap

import Core.CaseTree
import Core.Core
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Metadata
import Core.TT
import Core.UnifyState

import TTImp.TTImp

%default covering

showDefType : Def -> String
showDefType None = "undefined"
showDefType (PMDef {}) = "function"
showDefType (ExternDef {}) = "external function"
showDefType (ForeignDef {}) = "foreign function"
showDefType (Builtin {}) = "builtin function"
showDefType (DCon {}) = "data constructor"
showDefType (TCon {}) = "type constructor"
showDefType (Hole {}) = "hole"
showDefType (BySearch {}) = "search"
showDefType (Guess {}) = "guess"
showDefType ImpBind = "bound name"
showDefType Delayed = "delayed"

||| Get the return type.
getReturnType : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
getReturnType tm@(Bind _ x b scope) = case b of
    Let _ _ val _ => getReturnType $ subst {x} val scope
    Pi _ _ _ _ => getReturnType scope
    _ => Nothing
getReturnType tm = Just (vars ** tm)

||| Get the top level type constructor if there is one.
getTypeCons : {vars : _} -> Term vars -> Maybe Name
getTypeCons (Local _ _ _ p) = Just $ nameAt p
getTypeCons (Ref _ _ name) = Just name
getTypeCons (Meta {}) = Nothing
getTypeCons (Bind _ x b scope) = case b of
    Let _ _ val _ => getTypeCons $ subst {x} val scope
    _ => Nothing
getTypeCons (App _ fn _) = getTypeCons fn
getTypeCons _ = Nothing

||| Get the arguments of a `Term` representing a type.
getTypeArgs : {vars : _} -> Term vars -> List (vars ** Term vars)
getTypeArgs (Bind _ x b tm) = case b of
    Let _ _ val _ => getTypeArgs $ subst {x} val tm
    Pi _ _ _ arg => (_ ** arg) :: getTypeArgs tm
    _ => []
getTypeArgs _ = []

||| Get all non-erased aruments.
getNEArgs : {vars : _} -> Term vars -> List (vars ** Term vars)
getNEArgs (Bind _ x b tm) = case b of
    Let _ _ val _ => getNEArgs $ subst {x} val tm
    Pi _ mul _ arg => if isErased mul
        then getNEArgs tm
        else (_ ** arg) :: getNEArgs tm
    _ => []
getNEArgs _ = []

||| Get the first non-erased argument type.
getFirstNEType : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
getFirstNEType tm = case getNEArgs tm of
    [] => Nothing
    arg :: _ => Just arg

||| Get the index of the first non-erased argument if it exists.
getNEIndex : (arity : Nat) -> Term vars -> Maybe (Fin arity)
getNEIndex ar (Bind _ x b tm) = case b of
    Let _ _ val _ => getNEIndex ar $ subst {x} val tm
    Pi _ mul _ arg => if isErased mul
        then getNEIndex ar tm >>= Libs.strengthen . FS
        else natToFin 0 ar
    _ => Nothing
getNEIndex _ _ = Nothing

||| Get the index of all non-erased Integer argument.
getNEIntegerIndex : (arity : Nat) -> Term vars -> Maybe (List (Fin arity))
getNEIntegerIndex ar (Bind _ x b tm) = case b of
    Let _ _ val _ => getNEIntegerIndex ar $ subst {x} val tm
    Pi _ mul _ arg => if isRigOther mul && isInteger arg
        then case natToFin 0 ar of
            Nothing => Nothing
            Just idx => map (Prelude.(::) idx) $ go ar tm
        else go ar tm
    _ => Nothing
  where
    isInteger : forall vars. Term vars -> Bool
    isInteger (PrimVal _ IntegerType) = True
    isInteger _ = False
    go : forall vars. (sarity : Nat) -> Term vars -> Maybe (List (Fin sarity))
    go (S ar) tm = map FS <$> getNEIntegerIndex ar tm
    go Z _ = Just []
getNEIntegerIndex _ _ = Just []

||| Do the terms match ignoring arguments to type constructors.
termConMatch : Term vs -> Term vs' -> Bool
termConMatch (Local _ _ x _) (Local _ _ y _) = x == y
termConMatch (Ref _ _ n) (Ref _ _ m) = n == m
termConMatch (Meta _ _ i args0) (Meta _ _ j args1)
    = i == j && all (uncurry termConMatch) (zip args0 args1)
    -- I don't understand how they're equal if args are different lengths
    -- but this is what's in Core.TT.
termConMatch (Bind _ _ b s) (Bind _ _ c t) = eqBinderBy termConMatch b c && termConMatch s t
termConMatch (App _ f _) (App _ g _) = termConMatch f g
termConMatch (As _ _ a p) (As _ _ b q) = termConMatch a b && termConMatch p q
termConMatch (TDelayed _ _ tm0) tm1 = termConMatch tm0 tm1
termConMatch tm0 (TDelayed _ _ tm1) = termConMatch tm0 tm1
    -- don't check for laziness here to give more accurate error messages.
termConMatch (TDelay _ _ tm0 x0) (TDelay _ _ tm1 x1) = termConMatch tm0 tm1 && termConMatch x0 x1
termConMatch (TForce _ _ tm0) tm1 = termConMatch tm0 tm1
termConMatch tm0 (TForce _ _ tm1) = termConMatch tm0 tm1
termConMatch (PrimVal _ _) (PrimVal _ _) = True -- no constructor to check.
termConMatch (Erased _ _) (Erased _ _) = True -- return type can't erased?
termConMatch (TType _) (TType _) = True
termConMatch _ _ = False

||| Check a type is strict.
isStrict : Term vs -> Bool
isStrict (Local _ _ _ _) = True
isStrict (Ref _ _ _) = True
isStrict (Meta _ _ i args) = all isStrict args
isStrict (Bind _ _ b s) = isStrict (binderType b) && isStrict s
isStrict (App _ f x) = isStrict f && isStrict x
isStrict (As _ _ a p) = isStrict a && isStrict p
isStrict (TDelayed _ _ _) = False
isStrict (TDelay _ _ f x) = isStrict f && isStrict x
isStrict (TForce _ _ tm) = isStrict tm
isStrict (PrimVal _ _) = True
isStrict (Erased _ _) = True
isStrict (TType _) = True

getNatBuiltin : Ref Ctxt Defs => Name -> Core (Maybe NatBuiltin)
getNatBuiltin n = do
    n' <- getFullName n
    lookup n' . natTyNames . builtinTransforms <$> get Ctxt

||| Get the name and arity (of non-erased arguments only) of a list of names.
||| `cons` should all be data constructors (`DCon`) otherwise it will throw an error.
getConsGDef : Context -> FC -> (cons : List Name) -> Core $ List (Name, GlobalDef)
getConsGDef c fc = traverse \n => do
    [(n', _, gdef)] <- lookupCtxtName n c
        | [] => throw $ UndefinedName fc n
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    pure (n', gdef)

||| Check a list of constructors has exactly
||| 1 'Z'-like constructor
||| and 1 `S`-like constructor, which has type `ty -> ty` or `ty arg -> `ty (f arg)`.
checkNatCons : Context -> (cons : List (Name, GlobalDef)) -> (dataType : Name) -> FC -> Core NatBuiltin
checkNatCons c cons ty fc = case !(foldr checkCon (pure (Nothing, Nothing)) cons) of
    (Just zero, Just succ) => pure $ MkNatBuiltin {zero, succ}
    (Nothing, _) => throw $ GenericMsg fc $ "No 'Z'-like constructors for " ++ show ty ++ "."
    (_, Nothing) => throw $ GenericMsg fc $ "No 'S'-like constructors for " ++ show ty ++ "."
  where
    ||| Check if a list of names contains a name.
    checkSArgType : List Name -> Core ()
    checkSArgType [] = throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " is missing argument of type: " ++ show ty
    checkSArgType (n :: ns) = if nameRoot n == nameRoot ty && (n `matches` ty)
        then checkSArgType ns
        else throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " has unexpected argument: " ++ show n

    ||| Check the type of an 'S'-like constructor.
    checkTyS : Name -> GlobalDef -> Core ()
    checkTyS n gdef = do
        let type = gdef.type
            erase = gdef.eraseArgs
        let Just (_ ** arg) = getFirstNEType type
            | Nothing => throw $ InternalError "Expected a non-erased argument, found none."
        let Just (_ ** ret) = getReturnType type
            | Nothing => throw $ InternalError $ "Unexpected type " ++ show type
        unless (termConMatch arg ret) $ throw $ GenericMsg fc $ "Incorrect type for 'S'-like constructor for " ++ show ty ++ "."
        unless (isStrict arg) $ throw $ GenericMsg fc $ "Natural builtin does not support lazy types."
        pure ()

    ||| Check a constructor's arity and type.
    -- 'Z'-like constructor is always first, then 'S'-like constructor.
    checkCon : (Name, GlobalDef) -> Core (Maybe Name, Maybe Name) -> Core (Maybe Name, Maybe Name)
    checkCon (n, gdef) cons = do
        (zero, succ) <- cons
        let DCon _ arity _ = gdef.definition
            | def => throw $ GenericMsg fc $ "Expected data constructor, found:" ++ showDefType def
        case arity `minus` length gdef.eraseArgs of
            0 => case zero of
                Just _ => throw $ GenericMsg fc $ "Multiple 'Z'-like constructors for " ++ show ty ++ "."
                Nothing => pure (Just n, succ)
            1 => case succ of
                Just _ => throw $ GenericMsg fc $ "Multiple 'S'-like constructors for " ++ show ty ++ "."
                Nothing => do
                    checkTyS n gdef
                    pure (zero, Just n)
            _ => throw $ GenericMsg fc $ "Constructor " ++ show n ++ " doesn't match any pattern for Natural."

addBuiltinNat :
    Ref Ctxt Defs =>
    (ty : Name) -> NatBuiltin -> Core ()
addBuiltinNat type cons = do
    log "builtin.Natural.addTransform" 10
        $ "Add %builtin Natural transform for " ++ show type ++ "."
    update Ctxt $ record
        { builtinTransforms.natTyNames $= insert type cons
        , builtinTransforms.natZNames $= insert cons.zero MkZERO
        , builtinTransforms.natSNames $= insert cons.succ MkSUCC
        }

addNatToInteger :
    Ref Ctxt Defs =>
    (fn : Name) ->
    NatToInt ->
    Core ()
addNatToInteger fn nToI = do
    log "builtin.NaturalToInteger.addTransforms" 10
        $ "Add %builtin NaturalToInteger transform for " ++ show fn ++ "."
    update Ctxt $ record
        { builtinTransforms.natToIntegerFns $= insert fn nToI
        }

||| Check a `%builtin Natural` pragma is correct.
processBuiltinNatural :
    Ref Ctxt Defs =>
    Defs -> FC -> Name -> Core ()
processBuiltinNatural ds fc name = do
    log "builtin.Natural" 5 $ "Processing %builtin Natural " ++ show name ++ "."
    [(n, _, gdef)] <- lookupCtxtName name ds.gamma
        | [] => undefinedName fc name
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    let TCon _ _ _ _ _ _ dcons _ = gdef.definition
        | def => throw $ GenericMsg fc
            $ "Expected a type constructor, found " ++ showDefType def ++ "."
    cons <- getConsGDef ds.gamma fc dcons
    cons <- checkNatCons ds.gamma cons n fc
    zero <- getFullName cons.zero
    succ <- getFullName cons.succ
    addBuiltinNat n $ MkNatBuiltin {zero, succ}

||| Check a `%builtin NaturalToInteger` pragma is correct.
processNatToInteger :
    Ref Ctxt Defs =>
    Defs -> FC -> Name -> Core ()
processNatToInteger ds fc fn = do
    log "builtin.NaturalToInteger" 5 $ "Processing %builtin NaturalToInteger " ++ show fn ++ "."
    [(n, _, gdef)] <- lookupCtxtName fn ds.gamma
        | [] => undefinedName fc fn
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    let PMDef _ args _ cases _ = gdef.definition
        | def => throw $ GenericMsg fc
            $ "Expected function definition, found " ++ showDefType def ++ "."
    type <- toFullNames gdef.type
    logTerm "builtin.NaturalToInteger" 25 ("Type of " ++ show fn) type
    let [(_ ** arg)] = getNEArgs type
        | [] => throw $ GenericMsg fc $ "No arguments found for " ++ show n ++ "."
        | _ => throw $ GenericMsg fc $ "More than 1 non-erased arguments found for " ++ show n ++ "."
    let Just tyCon = getTypeCons arg
        | Nothing => throw $ GenericMsg fc
            $ "No type constructor found for non-erased arguement of " ++ show n ++ "."
    Just _ <- getNatBuiltin tyCon
        | Nothing => throw $ GenericMsg fc $ "Non-erased argument is not a 'Nat'-like type."
    let arity = length $ getTypeArgs type
    let Just natIdx = getNEIndex arity type
        | Nothing => throw $ InternalError "Couldn't find non-erased argument."
    addNatToInteger n (MkNatToInt arity natIdx)

addIntegerToNat :
    Ref Ctxt Defs =>
    (fn : Name) ->
    IntToNat ->
    Core ()
addIntegerToNat fn iToN = do
    log "builtin.IntegerToNatural.addTransforms" 10
        $ "Add %builtin IntegerToNatural transform for " ++ show fn ++ "."
    update Ctxt $ record
        { builtinTransforms.integerToNatFns $= insert fn iToN
        }

||| Check a `%builtin IntegerToNatural` pragma is correct.
processIntegerToNat :
    Ref Ctxt Defs =>
    Defs -> FC -> Name -> Core ()
processIntegerToNat ds fc fn = do
    log "builtin.IntegerToNatural" 5 $ "Processing %builtin IntegerToNatural " ++ show fn ++ "."
    [(n, _, gdef)] <- lookupCtxtName fn ds.gamma
        | [] => undefinedName fc fn
        | ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
    type <- toFullNames gdef.type
    let PMDef _ args _ cases _ = gdef.definition
        | def => throw $ GenericMsg fc
            $ "Expected function definition, found " ++ showDefType def ++ "."
    let arity = length $ getTypeArgs type
    logTerm "builtin.IntegerToNatural" 25 ("Type of " ++ show fn) type
    let Just [intIdx] = getNEIntegerIndex arity type
        | Just [] => throw $ GenericMsg fc $ "No unrestricted arguments of type `Integer` found for " ++ show n ++ "."
        | Just _ => throw $ GenericMsg fc $ "More than one unrestricted arguments of type `Integer` found for " ++ show n ++ "."
        | Nothing => throw $ InternalError
            $ "Unexpected arity while processing %builtin IntegerToNatural " ++ show n ++ " (getNEIntegerIndex returned Nothing)"
    let Just (_ ** retTy) = getReturnType type
        | Nothing => throw $ InternalError $ "Unexpected type " ++ show type
    let Just retCon = getTypeCons retTy
        | Nothing => throw $ GenericMsg fc
            $ "No type constructor found for return type of " ++ show n ++ "."
    Just _ <- getNatBuiltin retCon
        | Nothing => throw $ GenericMsg fc $ "Return type is not a 'Nat'-like type"
    addIntegerToNat n (MkIntToNat arity intIdx)

||| Check a `%builtin` pragma is correct.
export
processBuiltin :
    Ref Ctxt Defs =>
    NestedNames vars -> Env Term vars -> FC -> BuiltinType -> Name -> Core ()
processBuiltin nest env fc type name = do
    ds <- get Ctxt
    case type of
        BuiltinNatural => processBuiltinNatural ds fc name
        NaturalToInteger => processNatToInteger ds fc name
        IntegerToNatural => processIntegerToNat ds fc name

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module LazyPairingHeap

import Heap

%default total
%access private

export
data PairingHeap a = E | T a (PairingHeap a) (Lazy (PairingHeap a))

mutual
  link : Ord a => PairingHeap a -> PairingHeap a -> PairingHeap a
  link (T x E m) a = T x a m
  link (T x b m) a = T x E (assert_total $ merge (merge a b) m)
  link E         _ = assert_unreachable

  Heap PairingHeap where
    empty = E
    isEmpty E = True
    isEmpty _ = False

    insert x a = merge (T x E E) a

    merge a E = a
    merge E b = b
    merge a@(T x _ _) b@(T y _ _) = if x <= y then link a b else link b a

    findMin E = idris_crash "empty heap"
    findMin (T x a m) = x

    deleteMin E = idris_crash "empty heap"
    deleteMin (T x a m) = merge a m


text:
module TTImp.WithClause

import Core.Context
import Core.Context.Log
import Core.Metadata
import Core.TT

import TTImp.BindImplicits
import TTImp.TTImp
import TTImp.Elab.Check

import Data.List
import Data.Maybe

%default covering

matchFail : FC -> Core a
matchFail loc = throw (GenericMsg loc "With clause does not match parent")

--- To be used on the lhs of a nested with clause to figure out a tight location
--- information to give to the generated LHS
getHeadLoc : RawImp -> Core FC
getHeadLoc (IVar fc _) = pure fc
getHeadLoc (IApp _ f _) = getHeadLoc f
getHeadLoc (IAutoApp _ f _) = getHeadLoc f
getHeadLoc (INamedApp _ f _ _) = getHeadLoc f
getHeadLoc t = throw (InternalError $ "Could not find head of LHS: " ++ show t)

addAlias : {auto m : Ref MD Metadata} ->
           {auto c : Ref Ctxt Defs} ->
           FC -> FC -> Core ()
addAlias from to =
  whenJust (isConcreteFC from) $ \ from =>
    whenJust (isConcreteFC to) $ \ to => do
      log "ide-mode.highlight.alias" 25 $
        "Adding alias: " ++ show from ++ " -> " ++ show to
      addSemanticAlias from to

mutual
  export
  getMatch : {auto m : Ref MD Metadata} ->
             {auto c : Ref Ctxt Defs} ->
             (lhs : Bool) -> RawImp -> RawImp ->
             Core (List (String, RawImp))
  getMatch lhs (IBindVar to n) tm@(IBindVar from _)
      = [(n, tm)] <$ addAlias from to
  getMatch lhs (IBindVar _ n) tm = pure [(n, tm)]
  getMatch lhs (Implicit _ _) tm = pure []

  getMatch lhs (IVar to (NS ns n)) (IVar from (NS ns' n'))
      = if n == n' && isParentOf ns' ns
          then [] <$ addAlias from to -- <$ decorateName loc nm
          else matchFail from
  getMatch lhs (IVar to (NS ns n)) (IVar from n')
      = if n == n'
          then [] <$ addAlias from to -- <$ decorateName loc (NS ns n')
          else matchFail from
  getMatch lhs (IVar to n) (IVar from n')
      = if n == n'
          then [] <$ addAlias from to -- <$ decorateName loc n'
          else matchFail from
  getMatch lhs (IPi _ c p n arg ret) (IPi loc c' p' n' arg' ret')
      = if c == c' && eqPiInfoBy (\_, _ => True) p p' && n == n'
           then matchAll lhs [(arg, arg'), (ret, ret')]
           else matchFail loc
  -- TODO: Lam, Let, Case, Local, Update
  getMatch lhs (IApp _ f a) (IApp loc f' a')
      = matchAll lhs [(f, f'), (a, a')]
  getMatch lhs (IAutoApp _ f a) (IAutoApp loc f' a')
      = matchAll lhs [(f, f'), (a, a')]
  getMatch lhs (INamedApp _ f n a) (INamedApp loc f' n' a')
      = if n == n'
           then matchAll lhs [(f, f'), (a, a')]
           else matchFail loc
  getMatch lhs (IWithApp _ f a) (IWithApp loc f' a')
      = matchAll lhs [(f, f'), (a, a')]
  -- On LHS: If there's an implicit in the parent, but not the clause, add the
  -- implicit to the clause. This will propagate the implicit through to the
  -- body
  getMatch True (INamedApp fc f n a) f'
      = matchAll True [(f, f'), (a, a)]
  getMatch True (IAutoApp fc f a) f'
      = matchAll True [(f, f'), (a, a)]
  -- On RHS: Rely on unification to fill in the implicit
  getMatch False (INamedApp fc f n a) f'
      = getMatch False f f
  getMatch False (IAutoApp fc f a) f'
      = getMatch False f f
  -- Can't have an implicit in the clause if there wasn't a matching
  -- implicit in the parent
  getMatch lhs f (INamedApp fc f' n a)
      = matchFail fc
  getMatch lhs f (IAutoApp fc f' a)
      = matchFail fc
  -- Alternatives are okay as long as the alternatives correspond, and
  -- one of them is okay
  getMatch lhs (IAlternative fc _ as) (IAlternative _ _ as')
      = matchAny fc lhs (zip as as')
  getMatch lhs (IAs _ _ _ (UN (Basic n)) p) (IAs _ fc _ (UN (Basic n')) p')
      = do ms <- getMatch lhs p p'
           mergeMatches lhs ((n, IBindVar fc n') :: ms)
  getMatch lhs (IAs _ _ _ (UN (Basic n)) p) p'
      = do ms <- getMatch lhs p p'
           mergeMatches lhs ((n, p') :: ms)
  getMatch lhs (IAs _ _ _ _ p) p' = getMatch lhs p p'
  getMatch lhs p (IAs _ _ _ _ p') = getMatch lhs p p'
  getMatch lhs (IType _) (IType _) = pure []
  getMatch lhs (IPrimVal fc c) (IPrimVal fc' c') =
    if c == c'
    then pure []
    else matchFail fc
  getMatch lhs pat spec = matchFail (getFC pat)

  matchAny : {auto m : Ref MD Metadata} ->
             {auto c : Ref Ctxt Defs} ->
             FC -> (lhs : Bool) -> List (RawImp, RawImp) ->
             Core (List (String, RawImp))
  matchAny fc lhs [] = matchFail fc
  matchAny fc lhs ((x, y) :: ms)
      = catch (getMatch lhs x y)
              (\err => matchAny fc lhs ms)

  matchAll : {auto m : Ref MD Metadata} ->
             {auto c : Ref Ctxt Defs} ->
             (lhs : Bool) -> List (RawImp, RawImp) ->
             Core (List (String, RawImp))
  matchAll lhs [] = pure []
  matchAll lhs ((x, y) :: ms)
      = do matches <- matchAll lhs ms
           mxy <- getMatch lhs x y
           mergeMatches lhs (mxy ++ matches)

  mergeMatches : {auto m : Ref MD Metadata} ->
                 {auto c : Ref Ctxt Defs} ->
                 (lhs : Bool) -> List (String, RawImp) ->
                 Core (List (String, RawImp))
  mergeMatches lhs [] = pure []
  mergeMatches lhs ((n, tm) :: rest)
      = do rest' <- mergeMatches lhs rest
           case lookup n rest' of
                Nothing => pure ((n, tm) :: rest')
                Just tm' =>
                   do ignore $ getMatch lhs tm tm'
                      -- ^ just need to know it succeeds
                      pure rest'

-- Get the arguments for the rewritten pattern clause of a with by looking
-- up how the argument names matched
getArgMatch : FC -> (side : ElabMode) -> (search : Bool) ->
              (warg : RawImp) -> (matches : List (String, RawImp)) ->
              (arg : Maybe (PiInfo RawImp, Name)) -> RawImp
getArgMatch ploc mode search warg ms Nothing = warg
getArgMatch ploc mode True warg ms (Just (AutoImplicit, nm))
    = case (isUN nm >>= \ un => isBasic un >>= \ n => lookup n ms) of
        Just tm => tm
        Nothing =>
          let arg = ISearch ploc 500 in
          if isJust (isLHS mode)
            then IAs ploc ploc UseLeft nm arg
             else arg
getArgMatch ploc mode search warg ms (Just (_, nm))
    = case (isUN nm >>= \ un => isBasic un >>= \ n => lookup n ms) of
        Just tm => tm
        Nothing =>
          let arg = Implicit ploc True in
           if isJust (isLHS mode)
             then IAs ploc ploc UseLeft nm arg
             else arg

export
getNewLHS : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            FC -> (drop : Nat) -> NestedNames vars ->
            Name -> List (Maybe (PiInfo RawImp, Name)) ->
            RawImp -> RawImp -> Core RawImp
getNewLHS iploc drop nest wname wargnames lhs_raw patlhs
    = do let vploc = virtualiseFC iploc
         (mlhs_raw, wrest) <- dropWithArgs drop patlhs

         autoimp <- isUnboundImplicits
         setUnboundImplicits True
         (_, lhs) <- bindNames False lhs_raw
         (_, mlhs) <- bindNames False mlhs_raw
         setUnboundImplicits autoimp

         log "declare.def.clause.with" 20 $ "Parent LHS (with implicits): " ++ show lhs
         log "declare.def.clause.with" 20 $ "Modified LHS (with implicits): " ++ show mlhs

         let (warg :: rest) = reverse wrest
             | _ => throw (GenericMsg iploc "Badly formed 'with' clause")
         log "declare.def.clause.with" 5 $ show lhs ++ " against " ++ show mlhs ++
                 " dropping " ++ show (warg :: rest)
         ms <- getMatch True lhs mlhs
         log "declare.def.clause.with" 5 $ "Matches: " ++ show ms
         let params = map (getArgMatch vploc (InLHS top) False warg ms) wargnames
         log "declare.def.clause.with" 5 $ "Parameters: " ++ show params

         hdloc <- getHeadLoc patlhs
         let newlhs = apply (IVar hdloc wname) (params ++ rest)
         log "declare.def.clause.with" 5 $ "New LHS: " ++ show newlhs
         pure newlhs
  where
    dropWithArgs : Nat -> RawImp ->
                   Core (RawImp, List RawImp)
    dropWithArgs Z tm = pure (tm, [])
    dropWithArgs (S k) (IApp _ f arg)
        = do (tm, rest) <- dropWithArgs k f
             pure (tm, arg :: rest)
    -- Shouldn't happen if parsed correctly, but there's no guarantee that
    -- inputs come from parsed source so throw an error.
    dropWithArgs _ _ = throw (GenericMsg iploc "Badly formed 'with' clause")

-- Find a 'with' application on the RHS and update it
export
withRHS : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          FC -> (drop : Nat) -> Name -> List (Maybe (PiInfo RawImp, Name)) ->
          RawImp -> RawImp ->
          Core RawImp
withRHS fc drop wname wargnames tm toplhs
    = wrhs tm
  where
    withApply : FC -> RawImp -> List RawImp -> RawImp
    withApply fc f [] = f
    withApply fc f (a :: as) = withApply fc (IWithApp fc f a) as

    updateWith : FC -> RawImp -> List RawImp -> Core RawImp
    updateWith fc (IWithApp _ f a) ws = updateWith fc f (a :: ws)
    updateWith fc tm []
        = throw (GenericMsg fc "Badly formed 'with' application")
    updateWith fc tm (arg :: args)
        = do log "declare.def.clause.with" 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm
             ms <- getMatch False toplhs tm
             hdloc <- getHeadLoc tm
             log "declare.def.clause.with" 10 $ "Result: " ++ show ms
             let newrhs = apply (IVar hdloc wname)
                                (map (getArgMatch fc InExpr True arg ms) wargnames)
             log "declare.def.clause.with" 10 $ "With args for RHS: " ++ show wargnames
             log "declare.def.clause.with" 10 $ "New RHS: " ++ show newrhs
             pure (withApply fc newrhs args)

    mutual
      wrhs : RawImp -> Core RawImp
      wrhs (IPi fc c p n ty sc)
          = pure $ IPi fc c p n !(wrhs ty) !(wrhs sc)
      wrhs (ILam fc c p n ty sc)
          = pure $ ILam fc c p n !(wrhs ty) !(wrhs sc)
      wrhs (ILet fc lhsFC c n ty val sc)
          = pure $ ILet fc lhsFC c n !(wrhs ty) !(wrhs val) !(wrhs sc)
      wrhs (ICase fc sc ty clauses)
          = pure $ ICase fc !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)
      wrhs (ILocal fc decls sc)
          = pure $ ILocal fc decls !(wrhs sc) -- TODO!
      wrhs (IUpdate fc upds tm)
          = pure $ IUpdate fc upds !(wrhs tm) -- TODO!
      wrhs (IApp fc f a)
          = pure $ IApp fc !(wrhs f) !(wrhs a)
      wrhs (IAutoApp fc f a)
          = pure $ IAutoApp fc !(wrhs f) !(wrhs a)
      wrhs (INamedApp fc f n a)
          = pure $ INamedApp fc !(wrhs f) n !(wrhs a)
      wrhs (IWithApp fc f a) = updateWith fc f [a]
      wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)
      wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)
      wrhs (IDelay fc tm) = pure $ IDelay fc !(wrhs tm)
      wrhs (IForce fc tm) = pure $ IForce fc !(wrhs tm)
      wrhs tm = pure tm

      wrhsC : ImpClause -> Core ImpClause
      wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)
      wrhsC c = pure c


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

||| The original specification can be found at
||| https://infra.spec.whatwg.org/#namespaces
module API.Web.Infra.Namespaces

%access public export
%default total

html : String
html = "http://www.w3.org/1999/xhtml"

mathML : String
mathML = "http://www.w3.org/1998/Math/MathML"

svg : String
svg = "http://www.w3.org/2000/svg"

xLink : String
xLink = "http://www.w3.org/1999/xlink"

xml : String
xml = "http://www.w3.org/XML/1998/namespace"

xmlns : String
xmlns = "http://www.w3.org/2000/xmlns/"

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
module AppendVec

import Data.Vect

-- append : Vect n elem -> Vect m elem -> Vect (n + m) elem
-- append [] ys = ys
-- append (x :: xs) ys = x :: append xs ys

append_nil : (ys : Vect m elem) -> Vect (plus m 0) elem
append_nil {m} ys = rewrite plusZeroRightNeutral m in ys

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

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = append_nil ys
append (x :: xs) ys = append_xs (x :: append xs ys)

-- Ex 8.2 #1
myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes j@(S k) m = let p = myPlusCommutes k m in
                           rewrite p in rewrite (plusSuccRightSucc m k) in Refl

-- Ex 8.2 #2
reverseProof_Nil : Vect n1 a -> Vect (plus n1 0) a
reverseProof_Nil {n1} xs = rewrite plusZeroRightNeutral n1 in xs

reverseProof_xs : Vect ((S n1) + len) a -> Vect (plus n1 (S len)) a
reverseProof_xs {n1} {len} xs = rewrite sym (plusSuccRightSucc n1 len) in xs

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs
  where reverse' : Vect n a -> Vect m a -> Vect (n + m) a
        reverse' acc [] = reverseProof_Nil acc
        reverse' acc (x :: ys) = reverseProof_xs (reverse' (x :: acc) ys)


text:
module Text.WebIDL.Parser

import Data.SOP
import Data.List
import Data.List.Elem
import Data.List1
import Text.Lexer
import Text.Parser
import Text.WebIDL.Types
import Text.WebIDL.Lexer

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export
IdlGrammarAny : (b : Bool) -> Type -> Type
IdlGrammarAny b t = Grammar () IdlToken b t

public export
IdlGrammar : Type -> Type
IdlGrammar = IdlGrammarAny True

public export
IdlGrammar' : Type -> Type
IdlGrammar' = IdlGrammarAny False

tok : String -> (IdlToken -> Maybe a) -> IdlGrammar a
tok s f = terminal s f

withKey : String -> (String -> Maybe a) -> IdlGrammar a
withKey s f = tok s $ \case (Key $ MkKeyword s _) => f s
                            _                     => Nothing

intLit : IdlGrammar IntLit
intLit = tok "Int Lit" $ \case ILit n => Just n
                               _      => Nothing

stringLit : IdlGrammar StringLit
stringLit = tok "String Lit" $ \case SLit s => Just s
                                     _      => Nothing

floatLit : IdlGrammar FloatLit
floatLit = tok "Float Lit" $ \case FLit v => Just v
                                   _      => Nothing

--------------------------------------------------------------------------------
--          Symbols
--------------------------------------------------------------------------------

symbol : Char -> IdlGrammar ()
symbol c = tok ("Symbol " ++ show c) $ \case Other (Symb v) => guard (c == v)
                                             _              => Nothing

comma : IdlGrammar ()
comma = symbol ','

ellipsis : IdlGrammar ()
ellipsis = tok "Ellipsis" $ \case Other Ellipsis => Just ()
                                  _              => Nothing

inParens : {b : _} -> Inf (IdlGrammarAny b a) -> IdlGrammar a
inParens g = symbol '(' *> g <* symbol ')'

inBrackets : {b : _} -> Inf (IdlGrammarAny b a) -> IdlGrammar a
inBrackets g = symbol '[' *> g <* symbol ']'

inBraces : {b : _} -> Inf (IdlGrammarAny b a) -> IdlGrammar a
inBraces g = symbol '{' *> g <* symbol '}'

inAngles : {b : _} -> Inf (IdlGrammarAny b a) -> IdlGrammar a
inAngles g = symbol '<' *> g <* symbol '>'

inAnyParens : {b : _} -> Inf (IdlGrammarAny b a) -> IdlGrammar a
inAnyParens g = inParens g <|> inBrackets g <|> inBraces g

sepList1 : Char -> IdlGrammar a -> IdlGrammar (List1 a)
sepList1 c g =   [| (g <* symbol c) ::: sepBy (symbol c) g |]
             <|> map (\x => x ::: Nil) g

--------------------------------------------------------------------------------
--          Identifiers
--------------------------------------------------------------------------------

export
key : String -> IdlGrammar ()
key s = tok s $ \case Key (MkKeyword i _) => guard (i == s)
                      _                   => Nothing

export
ident : IdlGrammar Identifier
ident = tok "identifier" $ \case Ident i => Just i
                                 _       => Nothing

export
keyword : IdlGrammar Keyword
keyword = tok "keyword" $ \case Key i => Just i
                                _     => Nothing

||| IdentifierList :: identifier Identifiers
||| Identifiers :: , identifier Identifiers ε
export
identifierList : IdlGrammar IdentifierList
identifierList = [| ident ::: many (comma *> ident) |]

--------------------------------------------------------------------------------
--          Extended Attributes
--------------------------------------------------------------------------------

symbolUnless : String -> (Char -> Bool) -> IdlGrammar Symbol
symbolUnless s f = tok s $ \case Other s => fromSym s
                                 _       => Nothing
  where fromSym : Symbol -> Maybe Symbol
        fromSym Ellipsis = Just Ellipsis
        fromSym (Symb c) = if f c then Nothing else Just (Symb c)

otherSym : IdlGrammar Symbol -> IdlGrammar Other
otherSym sym = choice {t = List} [ map (\v => inject v) intLit
                                 , map (\v => inject v) stringLit
                                 , map (\v => inject v) floatLit
                                 , map (\v => inject v) ident
                                 , map (\v => inject v) sym
                                 , map (\v => inject v) keyword
                                 ]

export
other : IdlGrammar Other
other = otherSym $ symbolUnless "other" isCommaOrParenOrQuote

export
otherOrComma : IdlGrammar Other
otherOrComma = otherSym $ symbolUnless "otherOrComma" isParenOrQuote

export
eaInner : IdlGrammar' EAInner
eaInner =   [| EAIParens (inAnyParens eaInner) eaInner |]
        <|> [| EAIOther otherOrComma eaInner |]
        <|> pure EAIEmpty

export
extAttribute : IdlGrammar ExtAttribute
extAttribute =   [| EAParens (inAnyParens eaInner) (optional extAttribute) |]
             <|> [| EAOther other (optional extAttribute) |]

export
extAttrs1 : IdlGrammar ExtAttributeList
extAttrs1 = forget <$> inBrackets (sepBy1 comma extAttribute)

export
attributes : IdlGrammar' ExtAttributeList
attributes = extAttrs1 <|> pure Nil

export
attributed : IdlGrammar a -> IdlGrammar (Attributed a)
attributed g = [| (,) extAttrs1 g |] <|> map (Nil,) g

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

bufferRelated : IdlGrammar BufferRelatedType
bufferRelated = withKey "BufferRelated" $
                  \case "ArrayBuffer"       => Just ArrayBuffer
                        "DataView"          => Just DataView
                        "Int8Array"         => Just Int8Array
                        "Int16Array"        => Just Int16Array
                        "Int32Array"        => Just Int32Array
                        "Uint8Array"        => Just Uint8Array
                        "Uint16Array"       => Just Uint16Array
                        "Uint32Array"       => Just Uint32Array
                        "Uint8ClampedArray" => Just Uint8ClampedArray
                        "Float32Array"      => Just Float32Array
                        "Float64Array"      => Just Float64Array
                        _                   => Nothing

stringType : IdlGrammar StringType
stringType = withKey "stringType" $
               \case "ByteString" => Just ByteString
                     "DOMString"  => Just DOMString
                     "USVString"  => Just USVString
                     _            => Nothing

export
primitive : IdlGrammar PrimitiveType
primitive =   key "unsigned"     *> map Unsigned int
          <|> key "unrestricted" *> map Unrestricted float
          <|> map Signed int
          <|> map Restricted float
          <|> withKey "Primitive" (\case "boolean"   => Just Boolean
                                         "byte"      => Just Byte
                                         "octet"     => Just Octet
                                         "bigint"    => Just BigInt
                                         "undefined" => Just Undefined
                                         _           => Nothing)

  where int : IdlGrammar IntType
        int =   (key "long"  *> key "long" $> LongLong)
            <|> (key "long"  $> Long)
            <|> (key "short" $> Short)

        float : IdlGrammar FloatType
        float = withKey "FloatType" $ \case "double" => Just Dbl
                                            "float"  => Just Float
                                            _        => Nothing

constType : IdlGrammar ConstType
constType = map CP primitive <|> map CI ident

nullable : IdlGrammar a -> IdlGrammar (Nullable a)
nullable g = map MaybeNull (g <* symbol '?') <|> map NotNull g

mutual
  -- Type ::
  --     SingleType
  --     UnionType Null
  --
  -- SingleType ::
  --     DistinguishableType
  --     any
  --     PromiseType
  -- PromiseType ::
  --     Promise < Type >
  export
  idlType : IdlGrammar IdlType
  idlType =   (key "any" $> Any)
          <|> map Promise (key "Promise" *> inAngles idlType)
          <|> map D distinguishableType
          <|> (nullable flatUnion >>= map U . fromFlatUnion)

    where um : Attributed (Nullable Distinguishable) -> UnionMemberType
          um (a, MaybeNull x) = MkUnionMember a x
          um (a, NotNull x)   = MkUnionMember a x

          fromFlatUnion :  Nullable (List1 $ Attributed $ Nullable Distinguishable)
                        -> IdlGrammar' (Nullable UnionType)
          fromFlatUnion (MaybeNull $ a ::: b :: t) =
            pure . MaybeNull $ UT (um a) (um b) (map um t)

          fromFlatUnion (NotNull   $ a ::: b :: t) =
            if any (isNullable . snd) (a::b::t)
               then pure . MaybeNull $ UT (um a) (um b) (map um t)
               else pure . NotNull   $ UT (um a) (um b) (map um t)

          fromFlatUnion _                          = fail "no enough union members"

  -- TypeWithExtendedAttributes ::
  --     ExtendedAttributeList Type
  attrTpe : IdlGrammar (Attributed IdlType)
  attrTpe = attributed idlType

  -- RecordType ::
  --     record < StringType , TypeWithExtendedAttributes >
  recrd : IdlGrammar Distinguishable
  recrd = Record <$> (key "record" *> symbol '<' *> stringType)
                 <*> (comma *> attributes)
                 <*> (idlType <* symbol '>')

  -- DistinguishableType ::
  --     PrimitiveType Null
  --     StringType Null
  --     identifier Null
  --     sequence < TypeWithExtendedAttributes > Null
  --     object Null
  --     symbol Null
  --     BufferRelatedType Null
  --     FrozenArray < TypeWithExtendedAttributes > Null
  --     ObservableArray < TypeWithExtendedAttributes > Null
  --     RecordType Null
  distinguishable : IdlGrammar Distinguishable
  distinguishable =
        map P primitive
    <|> map S stringType
    <|> map B bufferRelated
    <|> (key "object" $> Object)
    <|> (key "symbol" $> Symbol)
    <|> (key "sequence" *> inAngles [| Sequence attributes idlType |])
    <|> (key "FrozenArray" *> inAngles [| FrozenArray attributes idlType |])
    <|> (key "ObservableArray" *> inAngles [| ObservableArray attributes idlType |])
    <|> recrd
    <|> map I ident

  distinguishableType : IdlGrammar (Nullable Distinguishable)
  distinguishableType = nullable distinguishable

  -- UnionType ::
  --     ( UnionMemberType or UnionMemberType UnionMemberTypes )
  --
  -- UnionMemberTypes ::
  --     or UnionMemberType UnionMemberTypes
  --     ε
  flatUnion : IdlGrammar (List1 $ Attributed $ Nullable Distinguishable)
  flatUnion = inParens $ do (a :: b :: t) <- sepBy (key "or") flatMember
                              | _ => fail "Non enough Union members"
                            pure (join $ a ::: b :: t)

  -- UnionMemberType ::
  --     ExtendedAttributeList DistinguishableType
  --     UnionType Null
  flatMember : IdlGrammar (List1 $ Attributed $ Nullable Distinguishable)
  flatMember = map singleton (attributed distinguishableType) <|> flatUnion

optionalType : IdlGrammar' OptionalType
optionalType = optional (symbol ',' *> attributed idlType)

--------------------------------------------------------------------------------
--          Arguments
--------------------------------------------------------------------------------

boolLit : IdlGrammar Bool
boolLit = (key "false" $> False) <|> (key "true" $> True)

constValue : IdlGrammar ConstValue
constValue = map B boolLit <|> map F floatLit <|> map I intLit

defaultV : IdlGrammar' Default
defaultV =   (symbol '=' *> (
                   (symbol '[' *> symbol ']' $> EmptyList)
               <|> (symbol '{' *> symbol '}' $> EmptySet)
               <|> (key "null" $> Null)
               <|> map S stringLit
               <|> map C constValue
             )) <|> pure None

argName : IdlGrammar ArgumentName
argName =   withKey "ArgumentNameKeyword"
              (map (MkArgName . value) . ArgumentNameKeyword.refine)
        <|> map (MkArgName . value) ident

arg : IdlGrammar Arg
arg = [| MkArg attributes idlType argName |]

vararg : IdlGrammar Arg
vararg = [| MkArg attributes (idlType <* ellipsis) argName |]

optArg : IdlGrammar OptArg
optArg = [| MkOptArg attributes
                     (key "optional" *> attributes)
                     idlType
                     argName
                     defaultV |]

argumentList : IdlGrammar' ArgumentList
argumentList =   [| VarArg args vararg |]
             <|> [| NoVarArg (args1 <* comma) (sepBy comma optArg) |]
             <|> [| NoVarArg args1 (pure Nil) |]
             <|> [| NoVarArg (pure Nil) (sepBy comma optArg) |]

  where args1 : IdlGrammar (List Arg)
        args1 = forget <$> sepBy1 comma arg

        args : IdlGrammar' (List Arg)
        args = (args1 <* comma) <|> pure Nil

optArgList : IdlGrammar' ArgumentList
optArgList = inParens argumentList <|> pure (NoVarArg Nil Nil)

--------------------------------------------------------------------------------
--          Member
--------------------------------------------------------------------------------

member : List String -> IdlGrammar a -> IdlGrammar a
member [] g = g <* symbol ';'
member (h :: t) g = key h *> member t g

export
const : IdlGrammar Const
const = member ["const"]
        [| MkConst constType ident (symbol '=' *> constValue) |]

special : IdlGrammar Special
special =   (key "getter"  $> Getter)
        <|> (key "setter"  $> Setter)
        <|> (key "deleter" $> Deleter)

opName : IdlGrammar OperationName
opName =   (key "includes" $> MkOpName "includes")
       <|> map (\(MkIdent s) => MkOpName s) ident

regularOperation : IdlGrammar RegularOperation
regularOperation =
  member []
  [| MkOp (pure ()) idlType (optional opName) (inParens argumentList) |]

specialOperation : IdlGrammar SpecialOperation
specialOperation =
  member []
  [| MkOp special idlType (optional opName) (inParens argumentList) |]

export
operation : IdlGrammar Operation
operation = map specToOp specialOperation <|> map regToOp regularOperation

callbackInterfaceMember : IdlGrammar CallbackInterfaceMember
callbackInterfaceMember =   map (\v => inject v) const
                        <|> map (\v => inject v) regularOperation

dictMember : IdlGrammar DictionaryMemberRest
dictMember = member ["required"] [| Required attributes idlType ident |]
           <|> member [] [| Optional idlType ident defaultV |]

inheritance : IdlGrammar' Inheritance
inheritance = optional (symbol ':' *> ident)

attributeName : IdlGrammar AttributeName
attributeName =  withKey "AttributeNameKeyword"
                   (map (MkAttributeName . value) . AttributeNameKeyword.refine)
             <|> map (MkAttributeName . value) ident

readonly : IdlGrammar a -> IdlGrammar (Readonly a)
readonly g = key "readonly" *> map MkRO g

inherit : IdlGrammar a -> IdlGrammar (Inherit a)
inherit g = key "inherit" *> map MkI g

attribute : IdlGrammar Attribute
attribute = member ["attribute"]
            [| MkAttribute attributes idlType attributeName |]

stringifier : IdlGrammar Stringifier
stringifier =   key "stringifier" *> (
                map (\v => inject v) attribute
            <|> map (\v => inject v) (readonly attribute)
            <|> map (\v => inject v) regularOperation
            <|> map (\v => inject v) (symbol ';')
            )

static : IdlGrammar StaticMember
static =   key "static" *> (
           map (\v => inject v) attribute
       <|> map (\v => inject v) (readonly attribute)
       <|> map (\v => inject v) regularOperation
       )

maplike : IdlGrammar Maplike
maplike = member ["maplike"] $ inAngles [| MkMaplike (attributed idlType)
                                        (symbol ',' *> attributed idlType) |]

setlike : IdlGrammar Setlike
setlike = member ["setlike"] $ inAngles [| MkSetlike (attributed idlType) |]

namespaceMember : IdlGrammar NamespaceMember
namespaceMember =   map (\v => inject v) regularOperation
                <|> map (\v => inject v) (readonly attribute)

constructor_ : IdlGrammar Constructor
constructor_ =
  member ["constructor"] (map MkConstructor $ inParens argumentList)

partialInterfaceMember : IdlGrammar PartialInterfaceMember
partialInterfaceMember =
      map IConst const
  <|> map IOp operation
  <|> map IAttr attribute
  <|> map IAttrRO (readonly attribute)
  <|> map IAttrInh (inherit attribute)
  <|> map IMap maplike
  <|> map IMapRO (readonly maplike)
  <|> map ISet setlike
  <|> map ISetRO (readonly setlike)
  <|> map IStr stringifier
  <|> map IStatic static
  <|> member ["iterable"] (inAngles [| IIterable (attributed idlType)
                                            optionalType |])
  <|> member ["async","iterable"] (
        do p  <- inAngles [| (,) (attributed idlType) optionalType |]
           as <- optArgList
           pure (IAsync (fst p) (snd p) as))

mixinMember : IdlGrammar MixinMember
mixinMember =   map MConst const
            <|> map MOp regularOperation
            <|> map MAttr attribute
            <|> map MAttrRO (readonly attribute)
            <|> map MStr stringifier

export
interfaceMember : IdlGrammar InterfaceMember
interfaceMember =   map (\v => inject v) constructor_
                <|> map (\v => inject v) partialInterfaceMember

members : IdlGrammar a -> IdlGrammar (List $ Attributed a)
members g = inBraces (many $ attributed g)

--------------------------------------------------------------------------------
--          Definition
--------------------------------------------------------------------------------

def :  (ss : List String)
    -> {auto 0 prf : NonEmpty ss}
    -> (IdlGrammar ExtAttributeList -> IdlGrammar a)
    -> IdlGrammar a
def (s :: ss) g = g (run ss (attributes <* key s)) <* symbol ';'
  where run : List String -> IdlGrammar x -> IdlGrammar x
        run []        y = y
        run (x :: xs) y = run xs (y <* key x)

def0 : (IdlGrammar' ExtAttributeList -> IdlGrammar a) -> IdlGrammar a
def0 g = g attributes <* symbol ';'

-- optional trailing comma
enumLits : IdlGrammar (List1 StringLit)
enumLits = sepList1 ',' stringLit <* (symbol ',' <|> pure ())

callback : IdlGrammar Callback
callback =
  def ["callback"] $ \as =>
  [| MkCallback as ident (symbol '=' *> idlType) (inParens argumentList) |]

callbackInterface : IdlGrammar CallbackInterface
callbackInterface =
  def ["callback","interface"] $ \as =>
  [| MkCallbackInterface as ident (members callbackInterfaceMember) |]

dictionary : IdlGrammar Dictionary
dictionary =
  def ["dictionary"] $ \as =>
  [| MkDictionary as ident inheritance (members dictMember) |]

enum : IdlGrammar Enum
enum = def ["enum"] $ \as => [| MkEnum as ident (inBraces enumLits) |]

iface : IdlGrammar Interface
iface =
  def ["interface"] $ \as =>
  [| MkInterface as ident inheritance (members interfaceMember) |]

includes : IdlGrammar Includes
includes =
  def0 $ \as => [| MkIncludes as ident (key "includes" *> ident) |]

mixin : IdlGrammar Mixin
mixin = def ["interface","mixin"] $ \as =>
        [| MkMixin as ident (members mixinMember) |]

nspace : IdlGrammar Namespace
nspace = def ["namespace"] $ \as =>
         [| MkNamespace as ident (members namespaceMember) |]

pdictionary : IdlGrammar PDictionary
pdictionary = def ["partial","dictionary"] $ \as =>
              [| MkPDictionary as ident (members dictMember) |]

pnamespace : IdlGrammar PNamespace
pnamespace = def ["partial","namespace"] $ \as =>
             [| MkPNamespace as ident (members namespaceMember) |]

pmixin : IdlGrammar PMixin
pmixin = def ["partial","interface","mixin"] $ \as =>
         [| MkPMixin as ident (members mixinMember) |]

pinterface : IdlGrammar PInterface
pinterface =
  def ["partial","interface"] $ \as =>
  [| MkPInterface as ident (members partialInterfaceMember) |]

typedef : IdlGrammar Typedef
typedef = def ["typedef"] $ \as =>
          [| MkTypedef as attributes idlType ident |]

export
definition : IdlGrammar Definition
definition =
      map (\v => inject v) callbackInterface
  <|> map (\v => inject v) callback
  <|> map (\v => inject v) dictionary
  <|> map (\v => inject v) enum
  <|> map (\v => inject v) iface
  <|> map (\v => inject v) includes
  <|> map (\v => inject v) mixin
  <|> map (\v => inject v) nspace
  <|> map (\v => inject v) typedef

export
part : IdlGrammar Part
part =   map (\v => inject v) pdictionary
     <|> map (\v => inject v) pinterface
     <|> map (\v => inject v) pmixin
     <|> map (\v => inject v) pnamespace

export
partsAndDefs : IdlGrammar PartsAndDefs
partsAndDefs = accumNs . forget <$> some partOrDef
  where partOrDef : IdlGrammar PartOrDef
        partOrDef =   map Z part
                  <|> map (S . Z) definition

--------------------------------------------------------------------------------
--          Parsing WebIDL
--------------------------------------------------------------------------------

toParseErr : ParsingError IdlToken -> Err
toParseErr (Error x Nothing)  = ParseErr x
toParseErr (Error x $ Just $ MkBounds startLine startCol _ _) =
  ParseErrAt x startLine startCol

export
parseIdl : IdlGrammar a -> String -> Either Err a
parseIdl g s = do ts <- mapFst LexErr (lexIdlNoNoise s)
                  (res,Nil) <- mapFst (toParseErr . head) (parse g ts)
                    | (_,b :: _) => Left (NoEOI b)
                  pure res