text:
module Quantities.Core

import public Quantities.FreeAbelianGroup
import public Quantities.Power

%default total
%access public export

||| Elementary quantities
record Dimension where
  constructor MkDimension
  name : String

implementation Eq Dimension where
  (MkDimension a) == (MkDimension b) = a == b

implementation Ord Dimension where
  compare (MkDimension a) (MkDimension b) = compare a b

-- Compound quantities

||| A quantity is a property that can be measured.
Quantity : Type
Quantity = FreeAbGrp Dimension

||| The trivial quantity
Scalar : Quantity
Scalar = unit

||| Create a new quantity.
mkQuantity : List (Dimension, Integer) -> Quantity
mkQuantity = mkFreeAbGrp

infixl 6 </>

-- Synonyms (quantites are multiplied, not added!)
||| Product quantity
(<*>) : Ord a => FreeAbGrp a -> FreeAbGrp a -> FreeAbGrp a
(<*>) = (<<+>>)

||| Quotient quantity
(</>) : Ord a => FreeAbGrp a -> FreeAbGrp a -> FreeAbGrp a
a </> b = a <*> freeAbGrpInverse b

||| Convert dimensions to quantities
implicit
dimensionToQuantity : Dimension -> Quantity
dimensionToQuantity = inject

||| Elementary Unit
record ElemUnit (q : Quantity) where
  constructor MkElemUnit
  name : String
  conversionRate : Double

-- ElemUnit with its quantity hidden
data SomeElemUnit : Type where
  MkSomeElemUnit : (q : Quantity) -> ElemUnit q -> SomeElemUnit

quantity : SomeElemUnit -> Quantity
quantity (MkSomeElemUnit q _) = q

elemUnit : (seu : SomeElemUnit) -> ElemUnit (quantity seu)
elemUnit (MkSomeElemUnit _ u) = u

name : SomeElemUnit -> String
name x = name (elemUnit x)

implementation Eq SomeElemUnit where
 a == b = quantity a == quantity b && name a == name b

implementation Ord SomeElemUnit where
  compare a b with (compare (quantity a) (quantity b))
    | LT = LT
    | GT = GT
    | EQ = compare (name a) (name b)

implicit
elemUnitToSomeElemUnitFreeAbGrp : ElemUnit q -> FreeAbGrp SomeElemUnit
elemUnitToSomeElemUnitFreeAbGrp {q} u = inject (MkSomeElemUnit q u)

conversionRate : SomeElemUnit -> Double
conversionRate u = conversionRate (elemUnit u)

joinedQuantity : FreeAbGrp SomeElemUnit -> Quantity
joinedQuantity = lift quantity

data Unit : Quantity -> Type where
  MkUnit : (exponent : Integer) -> (elemUnits : FreeAbGrp SomeElemUnit) ->
           Unit (joinedQuantity elemUnits)

rewriteUnit : r = q -> Unit q -> Unit r
rewriteUnit eq unit = rewrite eq in unit

base10Exponent : Unit q -> Integer
base10Exponent (MkUnit e _) = e

someElemUnitFreeAbGrp : Unit q -> FreeAbGrp SomeElemUnit
someElemUnitFreeAbGrp (MkUnit _ us) = us

implementation Eq (Unit q) where
  x == y = base10Exponent x == base10Exponent y &&
           someElemUnitFreeAbGrp x == someElemUnitFreeAbGrp y

||| The trivial unit
One : Unit Scalar
One = MkUnit 0 neutral

||| Multiples of ten
Ten : Unit Scalar
Ten = MkUnit 1 neutral

||| One hundredth
Percent : Unit Scalar
Percent = MkUnit (-2) neutral

||| One thousandth
Promille : Unit Scalar
Promille = MkUnit (-3) neutral

||| The trivial unit (synonymous with `one`)
UnitLess : Unit Scalar
UnitLess = One

implicit
elemUnitToUnit : {q : Quantity} -> ElemUnit q -> Unit q
elemUnitToUnit {q} u = rewriteUnit eq (MkUnit 0 (inject (MkSomeElemUnit q u)))
  where eq = sym (inject_lift_lem quantity (MkSomeElemUnit q u))

||| Compute conversion factor from the given unit to the base unit of the
||| corresponding quantity.
joinedConversionRate : Unit q -> Double
joinedConversionRate (MkUnit e (MkFreeAbGrp us)) = fromUnits * fromExponent
  where fromUnits    = product $ map (\(u, i) => ((^) @{floatmultpower}) (conversionRate u) i) us
        fromExponent = ((^) @{floatmultpower}) 10 e

||| Constructs a new unit given a name and conversion factor from an existing unit.
defineAsMultipleOf : String -> Double -> Unit q -> ElemUnit q
defineAsMultipleOf name factor unit = MkElemUnit name (factor * joinedConversionRate unit)

-- Syntax sugar for defining new units
syntax "< one" [name] equals [factor] [unit] ">" = defineAsMultipleOf name factor unit

implementation Show (Unit q) where
  show (MkUnit 0 (MkFreeAbGrp [])) = "unitLess"
  show (MkUnit e (MkFreeAbGrp [])) = "ten ^^ " ++ show e
  show (MkUnit e (MkFreeAbGrp (u :: us))) = if e == 0 then fromUnits
    else "ten ^^ " ++ show e ++ " <**> " ++ fromUnits
    where monom : (SomeElemUnit, Integer) -> String
          monom (unit, 1) = name unit
          monom (unit, i) = name unit ++ " ^^ " ++ show i
          fromUnits = monom u ++ concatMap ((" <**> " ++) . monom) us

||| Pretty-print a unit (using only ASCII characters)
showUnit : Unit q -> String
showUnit (MkUnit 0 (MkFreeAbGrp [])) = ""
showUnit (MkUnit e (MkFreeAbGrp [])) = "10^" ++ show e
showUnit (MkUnit e (MkFreeAbGrp (u :: us))) = if e == 0 then fromUnits
  else "10^" ++ show e ++ " " ++ fromUnits
  where monom : (SomeElemUnit, Integer) -> String
        monom (unit, 1) = name unit
        monom (unit, i) = name unit ++ "^" ++ show i
        fromUnits = monom u ++ concatMap ((" " ++) . monom) us

toSuperScript : Char -> Char
toSuperScript '1' = '¹'
toSuperScript '2' = '²'
toSuperScript '3' = '³'
toSuperScript '4' = '⁴'
toSuperScript '5' = '⁵'
toSuperScript '6' = '⁶'
toSuperScript '7' = '⁷'
toSuperScript '8' = '⁸'
toSuperScript '9' = '⁹'
toSuperScript '0' = '⁰'
toSuperScript '-' = '⁻'
toSuperScript x   = x

toSuper : String -> String
toSuper = pack . map toSuperScript . unpack

||| Pretty-print a unit
showUnitUnicode : Unit q -> String
showUnitUnicode (MkUnit 0 (MkFreeAbGrp [])) = ""
showUnitUnicode (MkUnit e (MkFreeAbGrp [])) = "10" ++ toSuper (show e)
showUnitUnicode (MkUnit e (MkFreeAbGrp (u :: us))) = if e == 0 then fromUnits
  else "10" ++ toSuper (show e) ++ " " ++ fromUnits
  where monom : (SomeElemUnit, Integer) -> String
        monom (unit, 1) = name unit
        monom (unit, i) = name unit ++ toSuper (show i)
        fromUnits = monom u ++ concatMap ((" " ++) . monom) us

infixr 10 ^^
||| Power unit
(^^) : Unit q -> (i : Integer) -> Unit (q ^ i)
(^^) (MkUnit e us) i = rewriteUnit eq (MkUnit (i*e) (us ^ i))
  where eq = sym (lift_power_lem quantity us i)

||| Inverse unit (e.g. the inverse of `second` is `one <//> second` a.k.a. `hertz`)
unitInverse : {q : Quantity} -> Unit q -> Unit (freeAbGrpInverse q)
unitInverse {q} u = rewrite (freeabgrppower_correct q (-1))
                    in u ^^ (-1)

infixl 6 <**>,<//>

||| Product unit
(<**>) : Unit r -> Unit s -> Unit (r <*> s)
(<**>) (MkUnit e rs) (MkUnit f ss) = rewriteUnit eq (MkUnit (e+f) (rs <*> ss))
  where eq = sym (lift_mult_lem quantity rs ss)

||| Quotient unit
(<//>) : Unit r -> Unit s -> Unit (r </> s)
(<//>) a b = a <**> unitInverse b

infixl 5 =| -- sensible?
||| Numbers tagged with a unit
data Measurement : {q : Quantity} -> Unit q -> Type -> Type where
  (=|) : a -> (u : Unit q) -> Measurement u a

||| Extract the number
getValue : {q : Quantity} -> {u : Unit q} ->
           Measurement {q} u a -> a
getValue (x =| _) = x

implementation Functor (Measurement {q} u) where
  map f (x =| _) = f x =| u

implementation Eq a => Eq (Measurement {q} u a) where
  (x =| _) == (y =| _) = x == y

implementation Ord a => Ord (Measurement {q} u a) where
  compare (x =| _) (y =| _) = compare x y

implementation Show a => Show (Measurement {q} u a) where
  show (x =| _) = show x ++ " =| " ++ show u

implementation Num a => Semigroup (Measurement {q} u a) where
  (x =| _) <+> (y =| _) = (x + y) =| u

implementation Num a => Monoid (Measurement {q} u a) where
  neutral = fromInteger 0 =| u

implementation (Neg a, Num a) => Group (Measurement {q} u a) where
  inverse (x =| _) = (-x) =| u

implementation (Neg a, Num a) => AbelianGroup (Measurement {q} u a) where

||| Pretty-print a measurement (using only ASCII characters)
showMeasurement : Show a => {q : Quantity} -> {u : Unit q} ->
                  (Measurement u a) -> String
showMeasurement (x =| u) =
  show x ++ (if base10Exponent u == 0 then " " else "*") ++ showUnit u

||| Pretty-print a measurement (using only ASCII characters)
showMeasurementUnicode : Show a => {q : Quantity} -> {u : Unit q} ->
                         (Measurement u a) -> String
showMeasurementUnicode (x =| u) =
  show x ++ (if base10Exponent u == 0 then " " else "·") ++ showUnit u

infixl 5 :|

||| Type synonym for `Measurement`
(:|) : Unit q -> Type -> Type
(:|) = Measurement

||| Flatten nested measurements
joinUnits : {q : Quantity} -> {r : Quantity} -> {u : Unit q} -> {v : Unit r} ->
            (u :| (v :| a)) -> (u <**> v) :| a
joinUnits ((x =| v) =| u) = x =| (u <**> v)

||| Double with a unit
F : Unit q -> Type
F u = Measurement u Double

infixl 9 |*|,|/|

||| Product measurement
(|*|) : Num a => {q : Quantity} -> {r : Quantity} -> {u : Unit q} -> {v : Unit r} ->
        u :| a -> v :| a -> (u <**> v) :| a
(|*|) (x =| u) (y =| v) = (x*y) =| (u <**> v)

||| Quotient measurement (the second measurement mustn't be zero!)
(|/|) : {q : Quantity} -> {r : Quantity} -> {u : Unit q} -> {v : Unit r} ->
        F u -> F v -> F (u <//> v)
(|/|) (x =| u) (y =| v) = (x/y) =| (u <//> v)

infixl 10 |^|

||| Power measurement
(|^|) : {q : Quantity} -> {u : Unit q} -> F u -> (i : Integer) -> F (u ^^ i)
(|^|) (x =| u) i = (((^) @{floatmultpower}) x i) =| u ^^ i

||| Square root measurement
sqrt : {q : Quantity} -> {u : Unit q} -> F (u ^^ 2) -> F u
sqrt {q} {u} (x =| _) = (sqrt x) =| u

||| Round measurement to the next integer below
floor : {q : Quantity} -> {u : Unit q} -> F u -> F u
floor = map floor

||| Round measurement to the next integer above
ceiling : {q : Quantity} -> {u : Unit q} -> F u -> F u
ceiling = map ceiling

||| Convert measurements to a given unit
convertTo : {from : Unit q} -> (to : Unit q) -> F from -> F to
convertTo to (x =| from) = (x * (rateFrom / rateTo)) =| to
  where rateFrom = joinedConversionRate from
        rateTo   = joinedConversionRate to

||| Flipped version of `convertTo`
as : {from : Unit q} -> F from -> (to : Unit q) -> F to
as x u = convertTo u x

||| Convert with implicit target unit
convert : {from : Unit q} -> {to : Unit q} -> F from -> F to
convert {to=to} x = convertTo to x

||| Promote values to measurements of the trivial quantity
implicit
toUnitLess : a -> Measurement unitLess a
toUnitLess x = x =| unitLess

implementation Num a => Num (Measurement unitLess a) where
  x + y = (getValue x + getValue y) =| unitLess
  x * y = (getValue x * getValue y) =| unitLess
  fromInteger i = fromInteger i =| unitLess

implementation Neg a => Neg (Measurement unitLess a) where
  negate x = negate (getValue x) =| unitLess
  x - y = (getValue x - getValue y) =| unitLess

implementation Abs a => Abs (Measurement unitLess a) where
  abs x = abs (getValue x) =| unitLess

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module wordlen

import Prelude
import Data.Vect

word_lengths' : Vect k String -> Vect k Nat
word_lengths' [] = [] -- Ctrl-Alt-S = search for a valid expression which satisfies that type
word_lengths' (x :: xs) = Strings.length x :: word_lengths' xs

word_lengths : List String -> List Nat
word_lengths [] = []
word_lengths (x :: xs) = Strings.length x :: word_lengths xs

isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not $ isEven k

ext: idr


text:
||| Reasoning about elements in a DList based on their index.
|||
||| Module    : DList/AtIndex.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Toolkit.Data.DList.AtIndex

import Decidable.Equality

import Toolkit.Decidable.Informative

import Toolkit.Data.List.AtIndex
import Toolkit.Data.DList

%default total

||| Proof that some element satisfies the predicate
|||
||| @idx   The type of the element's index.
||| @type  The type of the list element.
||| @p     A predicate
||| @xs      The list itself.
public export
data HoldsAtIndex : (type   : Type)
                 -> (item   : type -> Type)
                 -> (p      : {i : type} -> (x : item i) -> Type)
                 -> {is     : List type}
                 -> (xs     : DList type item is)
                 -> (idx    : Nat)
                           -> Type
    where
      ||| Proof that the element is at the front of the list.
      Here : {p   : {i : type} -> (x : item i) -> Type}
          -> {i   : type}
          -> {x   : item i}
          -> (prf : p x)
                 -> HoldsAtIndex type item p (x::xs) Z

      ||| Proof that the element is found later in the list.
      There : {p      : {i : type} -> (x : item i) -> Type}
           -> (contra : p x' -> Void)
           -> (later  : HoldsAtIndex type item p      xs     loc)
                     -> HoldsAtIndex type item p (x'::xs) (S loc)

namespace Find
  namespace HoldsAtIndex
    public export
    data Error type = IsEmpty
                    | Later type (HoldsAtIndex.Error type)

  isEmpty : {p  : {i : type} -> (x : item i) -> Type}
         -> DPair Nat (HoldsAtIndex type item p [])
         -> Void
  isEmpty (MkDPair loc prf) with (prf)
    isEmpty (MkDPair loc prf) | (MkDPair _ (Here _)) impossible
    isEmpty (MkDPair loc prf) | (MkDPair _ (There _)) impossible

  notLater : {p : {i : type} -> (x : item i) -> Type}
          -> (DPair Nat (HoldsAtIndex type item p rest) -> Void)
          -> (p i -> Void)
          -> DPair Nat (HoldsAtIndex type item p (i :: rest))
          -> Void
  notLater f g (MkDPair _ (Here prf))
    = g prf
  notLater f g (MkDPair _ (There contra later))
    = f (MkDPair _ later)

  export
  holdsAtIndex : {p  : {i : type} -> (x : item i) -> Type}
              -> (f  : {i : type} -> (x : item i) -> DecInfo err (p x))
              -> (xs : DList type item is)
                    -> DecInfo (HoldsAtIndex.Error err)
                               (DPair Nat (HoldsAtIndex type item p xs))
  holdsAtIndex f Nil
    = No IsEmpty (isEmpty)

  holdsAtIndex f (x :: y) with (f x)
    holdsAtIndex f (x :: y) | (Yes prf)
      = Yes (MkDPair 0 (Here prf))

    holdsAtIndex f (x :: y) | (No msg contra) with (holdsAtIndex f y)
      holdsAtIndex f (x :: y) | (No msg contra) | (Yes (MkDPair loc prf))
        = Yes (MkDPair (S loc) (There contra prf))

      holdsAtIndex f (x :: y) | (No msg contra) | (No msgR contraR)
        = No (Later msg msgR)
             (notLater contraR contra)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module ProofColDivSeqMain

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof
import Sub01Apply18x3
import Sub02Apply54x12
import Sub03Apply54x30
import Sub04Apply54x48
import Sub05Apply9x6
import Sub06Apply36x9
import Sub07Apply108x27
import Sub08Apply108x63
import Sub09Apply108x99
import Sub10Apply108x18
import Sub11Apply108x54
import Sub12Apply108x90
import Sub13Apply108x36
import Sub14Apply108x72
import Sub15Apply108x108

%default total
-- %language ElabReflection

-- 無限降下法の十分条件
unifi : (n:Nat) -> (Not . P) (S n) -> (m ** (LTE (S m) (S n), (Not . P) m))
unifi n prf with (mod3 n)
  unifi (j + j + j)         prf | ThreeZero with (parity j)
    unifi ((k+k) + (k+k) + (k+k))       prf | ThreeZero | Even = apply18x3 prf
    unifi (S (k+k) + S (k+k) + S (k+k)) prf | ThreeZero | Odd with (mod3 k)
      unifi (S ((l+l+l)+(l+l+l)) + S ((l+l+l)+(l+l+l)) + S ((l+l+l)+(l+l+l))) prf | ThreeZero | Odd | ThreeZero = apply54x12 prf
      unifi (S ((S (l+l+l))+(S (l+l+l))) + S ((S (l+l+l))+(S (l+l+l))) + S ((S (l+l+l))+(S (l+l+l)))) prf | ThreeZero | Odd | ThreeOne = apply54x30 prf
      unifi (S ((S (S (l+l+l)))+(S (S (l+l+l)))) + S ((S (S (l+l+l)))+(S (S (l+l+l)))) + S ((S (S (l+l+l)))+(S (S (l+l+l))))) prf | ThreeZero | Odd | ThreeTwo = apply54x48 prf
  unifi (S (j + j + j))     prf | ThreeOne = apply9x6 prf
  unifi (S (S (j + j + j))) prf | ThreeTwo with (parity j)
    unifi (S (S ((k+k) + (k+k) + (k+k)))) prf | ThreeTwo | Even with (parity k)
      unifi (S (S (((l+l)+(l+l)) + ((l+l)+(l+l)) + ((l+l)+(l+l))))) prf | ThreeTwo | Even | Even = apply36x9 prf
      unifi (S (S ((S (l+l)+S (l+l)) + (S (l+l)+S (l+l)) + (S (l+l)+S (l+l))))) prf | ThreeTwo | Even | Odd with (mod3 l)
        unifi (S (S ((S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o))) + (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o))) + (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o)))))) prf | ThreeTwo | Even | Odd | ThreeZero = apply108x27 prf
        unifi (S (S ((S (S (o+o+o)+S (o+o+o))+S (S (o+o+o)+ S (o+o+o))) + (S (S (o+o+o)+ S (o+o+o))+S (S (o+o+o)+ S (o+o+o))) + (S (S (o+o+o)+ S (o+o+o))+S (S (o+o+o)+ S (o+o+o)))))) prf | ThreeTwo | Even | Odd | ThreeOne = apply108x63 prf
        unifi (S (S ((S (S (S (o+o+o))+S (S (o+o+o)))+S (S (S (o+o+o))+ S (S (o+o+o))) + (S (S (S (o+o+o))+ S (S (o+o+o)))+S (S (S (o+o+o))+ S (S (o+o+o)))) + (S (S (S (o+o+o))+ S (S (o+o+o)))+S (S (S (o+o+o))+ S (S (o+o+o)))))))) prf | ThreeTwo | Even | Odd | ThreeTwo = apply108x99 prf
    unifi (S (S (S (k+k) + S (k+k) + S (k+k)))) prf | ThreeTwo | Odd with (parity k)
      unifi (S (S (S ((l+l)+(l+l)) + S ((l+l)+(l+l)) + S ((l+l)+(l+l))))) prf | ThreeTwo | Odd | Even with (mod3 l)
        unifi (S (S (S (((o+o+o)+(o+o+o))+((o+o+o)+(o+o+o))) + S (((o+o+o)+(o+o+o))+((o+o+o)+(o+o+o))) + S (((o+o+o)+(o+o+o))+((o+o+o)+(o+o+o)))))) prf | ThreeTwo | Odd | Even | ThreeZero = apply108x18 prf
        unifi (S (S (S ((S (o+o+o)+S (o+o+o))+(S (o+o+o)+S (o+o+o))) + S ((S (o+o+o)+S (o+o+o))+(S (o+o+o)+S (o+o+o))) + S ((S (o+o+o)+S (o+o+o))+(S (o+o+o)+S (o+o+o)))))) prf | ThreeTwo | Odd | Even | ThreeOne = apply108x54 prf
        unifi (S (S (S ((S (S (o+o+o))+S (S (o+o+o)))+(S (S (o+o+o))+S (S (o+o+o)))) + S ((S (S (o+o+o))+S (S (o+o+o)))+(S (S (o+o+o))+S (S (o+o+o)))) + S ((S (S (o+o+o))+S (S (o+o+o)))+(S (S (o+o+o))+S (S (o+o+o))))))) prf | ThreeTwo | Odd | Even | ThreeTwo = apply108x90 prf
      unifi (S (S (S (S (l+l)+ S (l+l)) + S (S (l+l)+S (l+l)) + S (S (l+l)+S (l+l))))) prf | ThreeTwo | Odd | Odd with (mod3 l)
        unifi (S (S (S (S ((o+o+o)+(o+o+o))+ S ((o+o+o)+(o+o+o))) + S (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o))) + S (S ((o+o+o)+(o+o+o))+S ((o+o+o)+(o+o+o)))))) prf | ThreeTwo | Odd | Odd | ThreeZero = apply108x36 prf
        unifi (S (S (S (S (S (o+o+o)+S (o+o+o))+ S (S (o+o+o)+S (o+o+o))) + S (S (S (o+o+o)+S (o+o+o))+S (S (o+o+o)+S (o+o+o))) + S (S (S (o+o+o)+S (o+o+o))+S (S (o+o+o)+S (o+o+o)))))) prf | ThreeTwo | Odd | Odd | ThreeOne = apply108x72 prf
        unifi (S (S (S (S (S (S (o+o+o))+S (S (o+o+o)))+ S (S (S (o+o+o))+S (S (o+o+o)))) + S (S (S (S (o+o+o))+S (S (o+o+o)))+S (S (S (o+o+o))+S (S (o+o+o)))) + S (S (S (S (o+o+o))+S (S (o+o+o)))+S (S (S (o+o+o))+S (S (o+o+o))))))) prf | ThreeTwo | Odd | Odd | ThreeTwo = apply108x108 prf

-- 最終的な定理
divSeqLimited : (n : Nat) -> Limited $ divSeq (n+n+n)
divSeqLimited n = replace (definiP n) {P=id} $ infiniteDescent0 unifi base0
                                    -- ↑このPはreplace内部のPだよ


text:
module Network.TLS.Verify

import Network.TLS.Core
import Network.TLS.Certificate
import Network.TLS.Signature
import Network.TLS.Handshake
import Network.TLS.Parse.DER
import Utils.Misc
import Utils.Bytes
import Data.String
import Data.List
import Data.List.Lazy
import Data.List1
import Data.Vect
import Utils.IPAddr
import Data.Either
import System
import Control.Monad.Error.Either
import Control.Monad.Trans

%hide Network.TLS.Handshake.Message.Certificate

||| Takes a wildcard domain like "*.google.com" and creates
||| a function to check if a string matches the wildcard domain
domain_predicate : String -> Maybe (String -> Bool)
domain_predicate predicate = do
  let parts = split ('.' ==) predicate
  guard $ verify_predicate parts
  Just (apply_predicate parts . split ('.' == ))
  where
    str_eq : String -> String -> Lazy Bool
    str_eq "*" _ = delay True
    str_eq _ "*" = delay True
    str_eq a b = delay (a == b)
    apply_predicate : List1 String -> List1 String -> Bool
    apply_predicate a b = (length a == length b) && (and $ zipWith str_eq a b)
    verify_predicate : List1 String -> Bool
    verify_predicate ("*" ::: []) = False
    verify_predicate ("*" ::: [_]) = False
    verify_predicate ("*" ::: [_, ""]) = False
    verify_predicate ("*" ::: xs) = and $ map (delay . not . isInfixOf "*") xs
    verify_predicate xs = and $ map (delay . not . isInfixOf "*") (toList xs)

domain_predicate' : String -> (String -> Bool)
domain_predicate' predicate =
  case domain_predicate predicate of
    Nothing => const False
    Just f => f

||| Type of identifier that will be used to check if a certificate's common name matches
||| the supplied hostname
Identifier : Type
Identifier = Eithers [IPv4Addr, IPv6Addr, String]

check_ipv4_address : List GeneralName -> IPv4Addr -> Bool
check_ipv4_address (IPv4Addr addr' :: xs) addr = if addr == addr' then True else check_ipv4_address xs addr
check_ipv4_address (x :: xs) addr = check_ipv4_address xs addr
check_ipv4_address [] _ = False

check_ipv6_address : List GeneralName -> IPv6Addr -> Bool
check_ipv6_address (IPv6Addr addr' :: xs) addr = if addr == addr' then True else check_ipv6_address xs addr
check_ipv6_address (x :: xs) addr = check_ipv6_address xs addr
check_ipv6_address [] _ = False

check_dns_name : List GeneralName -> String -> Bool
check_dns_name (DNSName predicate :: xs) name = if (domain_predicate' predicate) name then True else check_dns_name xs name
check_dns_name (x :: xs) name = check_dns_name xs name
check_dns_name [] _ = False

||| Check if the certificate has expired
check_cert_timestamp : HasIO io => Certificate -> io Bool
check_cert_timestamp cert = (\t => t > cert.valid_not_before && t < cert.valid_not_after) <$> time

||| Find a certificate with matching common name given an identifier
find_certificate : Identifier -> List Certificate -> Maybe Certificate
find_certificate identifier certs = choice $ map (delay . is_certificate identifier) certs
  where
    is_certificate : Identifier -> Certificate -> Maybe Certificate
    is_certificate (Left x)          cert = guard (check_ipv4_address (certificate_subject_names cert) x) $> cert
    is_certificate (Right (Left x))  cert = guard (check_ipv6_address (certificate_subject_names cert) x) $> cert
    is_certificate (Right (Right x)) cert = guard (check_dns_name (certificate_subject_names cert) x) $> cert

||| Convert a string of hostname into an identifier, such as DNSName, IPv4 and IPv6 address
to_identifier : String -> Identifier
to_identifier hostname =
  case parse_ipv4 hostname of
    Right x => Left x
    Left _ =>
      case parse_ipv6 hostname of
        Right x => Right (Left x)
        Left _ => Right (Right hostname)

||| Check if the server's certificate is valid
check_leaf_certificate : HasIO io => Certificate -> EitherT String io ()
check_leaf_certificate cert = do
  True <- check_cert_timestamp cert
  | False => throwE $ "expired certificate: " <+> show cert
  let Just key_usage = extract_extension KeyUsage cert
  | Nothing => throwE $ "certificate does not specify key usage: " <+> show cert
  let True = key_usage.digital_signature
  | False => throwE $ "certificate key usage does not allow digital signature: " <+> show cert
  pure ()

||| Check if the server's certificate's ca and intermediate ca's are valid
||| depth refers to how deep you are in the certificate chain, needed since
||| some intermediate ca's specify a constraint on the maximum depth
check_branch_certificate : HasIO io => Nat -> Certificate -> EitherT String io ()
check_branch_certificate depth cert = do
  True <- check_cert_timestamp cert
  | False => throwE $ "expired certificate: " <+> show cert
  let Just key_usage = extract_extension KeyUsage cert
  | Nothing => throwE $ "certificate does not specify key usage: " <+> show cert
  let Just basic_constraint = extract_extension BasicConstraint cert
  | Nothing => throwE $ "certificate does not specify basic constraint: " <+> show cert
  let True = basic_constraint.ca
  | False => throwE $ "certificate is not a CA: " <+> show cert
  let True = basic_constraint.path_len `cmp` depth
  | False => throwE $ "certificate CA depth reached: " <+> show cert
  let True = key_usage.key_cert_sign
  | False => throwE $ "certificate key usage does not allow signing certificates: " <+> show cert
  pure ()
  where
    cmp : Maybe Nat -> Nat -> Bool
    cmp Nothing _ = True
    cmp (Just a) b = b <= a

||| Given a certificate and its issuer's certificate, verify if the certificate's signature is correct
verify_certificate_signature : Certificate -> Certificate -> Either String ()
verify_certificate_signature subject issuer = bimap ("error at \{show subject}: " <+>) id $
  verify_signature' subject.sig_parameter issuer.cert_public_key subject.tbs_raw_bytes subject.signature_value

||| True if there is intersecting elements in both list
has_intersect : Eq a => List a -> List a -> Bool
has_intersect [] y = False
has_intersect x [] = False
has_intersect (x :: xs) y = if any (x ==) y then True else has_intersect xs y

||| Given an Authority Key Identifier extension, verifies if another certificate matches the constraint
||| This is needed since in the case that a certificate is cross signed by another CA, issuer and subject
||| distinguished names are not sufficient to find a subject's issuer.
auth_key_id_predicate : ExtAuthorityKeyIdentifier -> (Certificate -> Bool)
auth_key_id_predicate (MkExtAuthorityKeyIdentifier Nothing [] Nothing) = const False
auth_key_id_predicate auth_key_id = go auth_key_id
  where
    def : Maybe Bool -> Bool
    def Nothing = True
    def (Just a) = a
    -- Check if the SHA1 hash of public keys match
    go0 : ExtAuthorityKeyIdentifier -> Certificate -> Bool
    go0 auth_key_id cert = def (map (\i => i == cert.cert_public_key_id) auth_key_id.key_identifier)
    -- Check if the serial number matches
    go1 : ExtAuthorityKeyIdentifier -> Certificate -> Bool
    go1 auth_key_id cert = def (map (\i => i == cert.serial_number) auth_key_id.serial_number)
    -- Check if the subject distinguished names match
    go2 : ExtAuthorityKeyIdentifier -> Certificate -> Bool
    go2 auth_key_id cert =
      case auth_key_id.general_names of
        [] => True
        gn => has_intersect gn $ certificate_subject_names cert
    go : ExtAuthorityKeyIdentifier -> Certificate -> Bool
    go a b = go0 a b && go1 a b && go2 a b

flatten : Maybe (LazyList a) -> LazyList a
flatten Nothing = []
flatten (Just a) = a

liftE : Monad m => Either a b -> EitherT a m b
liftE x = MkEitherT $ pure x

verify_certificate_chain : HasIO io => Nat -> List Certificate -> List Certificate -> Certificate -> EitherT String io ()
verify_certificate_chain depth trusted untrusted current = do
  -- Constructs a lazy list of ca's which have cross signed the current certificate
  -- Won't be used if the certificate has a valid issuer which is in the chain
  let alternate = map (True,) $ flatten $ do
    ext <- extract_extension AuthorityKeyIdentifier current
    let predicate = auth_key_id_predicate ext
    pure $ filter predicate $ Lazy.fromList trusted

  -- List of certificates which subject name matches the current certificate's issuser name
  let in_chain = filter (\(_,c) => c.subject == current.issuer) (map (False,) untrusted <+> map (True,) trusted)
  let all_candidates = fromList in_chain <+> alternate

  case all_candidates of
    [] => throwE $ "cannot find issuer for: " <+> show current
    all => Lazy.choice $ map (\(should_trust,next) => go should_trust next current) all
  where
    -- Verify the issuer certificate and the subject's signature
    go : Bool -> Certificate -> Certificate -> EitherT String io ()
    go should_trust next current =
      case should_trust of
        False => do
          check_branch_certificate depth next
          let Right () = verify_certificate_signature current next
          | Left err => throwE $ "certificate failed for subject: " <+> show current <+> ", issuer: " <+> show next <+> ", reason " <+> err
          verify_certificate_chain (S depth) trusted untrusted next
        True => do
          -- replace the self signed certificate with the one in the trusted certificate list
          -- this should works since they are the same
          -- this prevents an attacker modifying the content of the certificate chain, changing the
          -- root ca's certificate with their own, with the same subject name but different public key
          let Just next = find (\c => c.subject == next.subject) trusted
          | Nothing => throwE $ "root certificate not trusted: " <+> show next
          check_branch_certificate depth next
          let Right () = verify_certificate_signature current next
          | Left err => throwE $ "certificate failed for subject: " <+> show current <+> ", issuer: " <+> show next <+> ", reason " <+> err
          pure ()

||| Given a list of trusted certificate, hostname of the server, verify the certificate chain
||| and return a public key to be used to verify TLS handshake
export
certificate_check : List Certificate -> String -> CertificateCheck IO
certificate_check trusted hostname cert = runEitherT $ do
  let certificates = body <$> cert.certificates
  ok <- liftE $ the _ $ traverse parse_certificate certificates
  let identifer = to_identifier hostname
  let Just cert = find_certificate identifer ok
  | Nothing => throwE "cannot find certificate"
  check_leaf_certificate cert
  verify_certificate_chain Z trusted ok cert
  pure cert.cert_public_key

||| A CertificateCheck function that always trusts the certificate unless it's malformed
export
certificate_ignore_check : String -> CertificateCheck IO
certificate_ignore_check hostname cert = runEitherT $ do
  let certificates = body <$> cert.certificates
  ok <- liftE $ the _ $ traverse parse_certificate certificates
  let identifer = to_identifier hostname
  let Just cert = find_certificate identifer ok
  | Nothing => throwE "cannot find certificate"
  pure cert.cert_public_key


text:
module Dbcritic.Check

import Control.IOExcept
import Dbcritic.Interface
import Dbcritic.Libpq

public export
record Issue where
    constructor MkIssue

    identifier    : List String
    description   : String
    problems      : List String
    solutions     : List String

    identifier_ne : NonEmpty identifier
    problems_ne   : NonEmpty problems
    solutions_ne  : NonEmpty solutions

public export
record Check where
    constructor MkCheck
    identifier : String
    help       : String
    inspect    : PgConnection -> IOExcept String (List Issue)

||| The qualified identifier of an issue incorporates both
||| the identifier of the check and the identifier of the issue.
qualified : Check -> Issue -> List String
qualified check issue = identifier check :: identifier issue

export
formatIssue : Int -> Check -> Issue -> String
formatIssue index check issue =
    formatMessage index (description issue) (problems issue) (solutions issue ++ [silenceIssue, silenceCheck])
    where
    silenceIssue = "Silence this issue: ‘silence " ++ unwords (qualified check issue) ++ "’."
    silenceCheck = "Silence this check: ‘silence " ++ identifier check ++ "’."

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
module Network.Curl.Types.CurlECode

import  Network.Curl.Types.Code

import Util

import Derive.Enum
%language ElabReflection

public export
data CurlECode
  = CURLE_OK                      {- 0 -}
  | CURLE_UNSUPPORTED_PROTOCOL    {- 1 -}
  | CURLE_FAILED_INIT             {- 2 -}
  | CURLE_URL_MALFORMAT           {- 3 -}
  | CURLE_NOT_BUILT_IN            {- 4 - [was obsoleted in August 2007 for
                                    7.17.0, reused in April 2011 for 7.21.5] -}
  | CURLE_COULDNT_RESOLVE_PROXY   {- 5 -}
  | CURLE_COULDNT_RESOLVE_HOST    {- 6 -}
  | CURLE_COULDNT_CONNECT         {- 7 -}
  | CURLE_WEIRD_SERVER_REPLY      {- 8 -}
  | CURLE_REMOTE_ACCESS_DENIED    {- 9 a service was denied by the server
                                    due to lack of access - when login fails
                                    this is not returned. -}
  | CURLE_FTP_ACCEPT_FAILED       {- 10 - [was obsoleted in April 2006 for
                                    7.15.4, reused in Dec 2011 for 7.24.0]-}
  | CURLE_FTP_WEIRD_PASS_REPLY    {- 11 -}
  | CURLE_FTP_ACCEPT_TIMEOUT      {- 12 - timeout occurred accepting server
                                    [was obsoleted in August 2007 for 7.17.0,
                                    reused in Dec 2011 for 7.24.0]-}
  |CURLE_FTP_WEIRD_PASV_REPLY    {- 13 -}
  |CURLE_FTP_WEIRD_227_FORMAT    {- 14 -}
  |CURLE_FTP_CANT_GET_HOST       {- 15 -}
  |CURLE_HTTP2                   {- 16 - A problem in the http2 framing layer.
                                    [was obsoleted in August 2007 for 7.17.0,
                                    reused in July 2014 for 7.38.0] -}
  | CURLE_FTP_COULDNT_SET_TYPE    {- 17 -}
  | CURLE_PARTIAL_FILE            {- 18 -}
  | CURLE_FTP_COULDNT_RETR_FILE   {- 19 -}
  | CURLE_OBSOLETE20              {- 20 - NOT USED -}
  | CURLE_QUOTE_ERROR             {- 21 - quote command failure -}
  | CURLE_HTTP_RETURNED_ERROR     {- 22 -}
  | CURLE_WRITE_ERROR             {- 23 -}
  | CURLE_OBSOLETE24              {- 24 - NOT USED -}
  | CURLE_UPLOAD_FAILED           {- 25 - failed upload "command" -}
  | CURLE_READ_ERROR              {- 26 - couldn't open/read from file -}
  | CURLE_OUT_OF_MEMORY           {- 27 -}
  {- Note: CURLE_OUT_OF_MEMORY may sometimes indicate a conversion error
           instead of a memory allocation error if CURL_DOES_CONVERSIONS
           is defined
  -}
  | CURLE_OPERATION_TIMEDOUT      {- 28 - the timeout time was reached -}
  | CURLE_OBSOLETE29              {- 29 - NOT USED -}
  | CURLE_FTP_PORT_FAILED         {- 30 - FTP PORT operation failed -}
  | CURLE_FTP_COULDNT_USE_REST    {- 31 - the REST command failed -}
  | CURLE_OBSOLETE32              {- 32 - NOT USED -}
  | CURLE_RANGE_ERROR             {- 33 - RANGE "command" didn't work -}
  | CURLE_HTTP_POST_ERROR         {- 34 -}
  | CURLE_SSL_CONNECT_ERROR       {- 35 - wrong when connecting with SSL -}
  | CURLE_BAD_DOWNLOAD_RESUME     {- 36 - couldn't resume download -}
  | CURLE_FILE_COULDNT_READ_FILE  {- 37 -}
  | CURLE_LDAP_CANNOT_BIND        {- 38 -}
  | CURLE_LDAP_SEARCH_FAILED      {- 39 -}
  | CURLE_OBSOLETE40              {- 40 - NOT USED -}
  | CURLE_FUNCTION_NOT_FOUND      {- 41 - NOT USED starting with 7.53.0 -}
  | CURLE_ABORTED_BY_CALLBACK     {- 42 -}
  | CURLE_BAD_FUNCTION_ARGUMENT   {- 43 -}
  | CURLE_OBSOLETE44              {- 44 - NOT USED -}
  | CURLE_INTERFACE_FAILED        {- 45 - CURLOPT_INTERFACE failed -}
  | CURLE_OBSOLETE46              {- 46 - NOT USED -}
  | CURLE_TOO_MANY_REDIRECTS      {- 47 - catch endless re-direct loops -}
  | CURLE_UNKNOWN_OPTION          {- 48 - User specified an unknown option -}
  | CURLE_TELNET_OPTION_SYNTAX    {- 49 - Malformed telnet option -}
  | CURLE_OBSOLETE50              {- 50 - NOT USED -}
  | CURLE_OBSOLETE51              {- 51 - NOT USED -}
  | CURLE_GOT_NOTHING             {- 52 - when this is a specific error -}
  | CURLE_SSL_ENGINE_NOTFOUND     {- 53 - SSL crypto engine not found -}
  | CURLE_SSL_ENGINE_SETFAILED    {- 54 - can not set SSL crypto engine as
                                    default -}
  | CURLE_SEND_ERROR              {- 55 - failed sending network data -}
  | CURLE_RECV_ERROR              {- 56 - failure in receiving network data -}
  | CURLE_OBSOLETE57              {- 57 - NOT IN USE -}
  | CURLE_SSL_CERTPROBLEM         {- 58 - problem with the local certificate -}
  | CURLE_SSL_CIPHER              {- 59 - couldn't use specified cipher -}
  | CURLE_PEER_FAILED_VERIFICATION {- 60 - peer's certificate or fingerprint
                                     wasn't verified fine -}
  | CURLE_BAD_CONTENT_ENCODING    {- 61 - Unrecognized/bad encoding -}
  | CURLE_LDAP_INVALID_URL        {- 62 - Invalid LDAP URL -}
  | CURLE_FILESIZE_EXCEEDED       {- 63 - Maximum file size exceeded -}
  | CURLE_USE_SSL_FAILED          {- 64 - Requested FTP SSL level failed -}
  | CURLE_SEND_FAIL_REWIND        {- 65 - Sending the data requires a rewind
                                    that failed -}
  | CURLE_SSL_ENGINE_INITFAILED   {- 66 - failed to initialise ENGINE -}
  | CURLE_LOGIN_DENIED            {- 67 - user, password or similar was not
                                    accepted and we failed to login -}
  | CURLE_TFTP_NOTFOUND           {- 68 - file not found on server -}
  | CURLE_TFTP_PERM               {- 69 - permission problem on server -}
  | CURLE_REMOTE_DISK_FULL        {- 70 - out of disk space on server -}
  | CURLE_TFTP_ILLEGAL            {- 71 - Illegal TFTP operation -}
  | CURLE_TFTP_UNKNOWNID          {- 72 - Unknown transfer ID -}
  | CURLE_REMOTE_FILE_EXISTS      {- 73 - File already exists -}
  | CURLE_TFTP_NOSUCHUSER         {- 74 - No such user -}
  | CURLE_CONV_FAILED             {- 75 - conversion failed -}
  | CURLE_CONV_REQD               {- 76 - caller must register conversion
                                    callbacks using curl_easy_setopt options
                                    CURLOPT_CONV_FROM_NETWORK_FUNCTION,
                                    CURLOPT_CONV_TO_NETWORK_FUNCTION, and
                                    CURLOPT_CONV_FROM_UTF8_FUNCTION -}
  | CURLE_SSL_CACERT_BADFILE      {- 77 - could not load CACERT file, missing
                                    or wrong format -}
  | CURLE_REMOTE_FILE_NOT_FOUND   {- 78 - remote file not found -}
  | CURLE_SSH                     {- 79 - error from the SSH layer, somewhat
                                    generic so the error message will be of
                                    interest when this has happened -}

  | CURLE_SSL_SHUTDOWN_FAILED     {- 80 - Failed to shut down the SSL
                                    connection -}
  | CURLE_AGAIN                   {- 81 - socket is not ready for send/recv,
                                    wait till it's ready and try again (Added
                                    in 7.18.2) -}
  | CURLE_SSL_CRL_BADFILE         {- 82 - could not load CRL file, missing or
                                    wrong format (Added in 7.19.0) -}
  | CURLE_SSL_ISSUER_ERROR        {- 83 - Issuer check failed.  (Added in
                                    7.19.0) -}
  | CURLE_FTP_PRET_FAILED         {- 84 - a PRET command failed -}
  | CURLE_RTSP_CSEQ_ERROR         {- 85 - mismatch of RTSP CSeq numbers -}
  | CURLE_RTSP_SESSION_ERROR      {- 86 - mismatch of RTSP Session Ids -}
  | CURLE_FTP_BAD_FILE_LIST       {- 87 - unable to parse FTP file list -}
  | CURLE_CHUNK_FAILED            {- 88 - chunk callback reported error -}
  | CURLE_NO_CONNECTION_AVAILABLE {- 89 - No connection available, the
                                    session will be queued -}
  | CURLE_SSL_PINNEDPUBKEYNOTMATCH {- 90 - specified pinned public key did not
                                     match -}
  | CURLE_SSL_INVALIDCERTSTATUS   {- 91 - invalid certificate status -}
  | CURLE_HTTP2_STREAM            {- 92 - stream error in HTTP/2 framing layer
                                    -}
  | CURLE_RECURSIVE_API_CALL      {- 93 - an api function was called from
                                    inside a callback -}
  | CURLE_AUTH_ERROR              {- 94 - an authentication function returned an
                                    error -}
  | CURLE_HTTP3                   {- 95 - An HTTP/3 layer problem -}
  | CURL_LAST {- never use! -}

public export
data GlobalFlag : Type where
  CURL_GLOBAL_SSL : GlobalFlag -- (1<<0) /* no purpose since since 7.57.0 */
  CURL_GLOBAL_WIN32 : GlobalFlag -- (1<<1)
  CURL_GLOBAL_ALL : GlobalFlag -- (CURL_GLOBAL_SSL|CURL_GLOBAL_WIN32)
  CURL_GLOBAL_NOTHING : GlobalFlag -- 0
  CURL_GLOBAL_DEFAULT : GlobalFlag -- CURL_GLOBAL_ALL
  CURL_GLOBAL_ACK_EINTR : GlobalFlag -- (1<<2)

export
ToCode GlobalFlag where
  toCode CURL_GLOBAL_SSL = 1
  toCode CURL_GLOBAL_WIN32 = 2
  toCode CURL_GLOBAL_ALL = 3
  toCode CURL_GLOBAL_NOTHING = 0
  toCode CURL_GLOBAL_DEFAULT = 3
  toCode CURL_GLOBAL_ACK_EINTR = 4

-- export
-- FromCode GlobalFlag where
--   fromCode 1 = CURL_GLOBAL_SSL
--   fromCode 2 = CURL_GLOBAL_WIN32
--   fromCode 3 = CURL_GLOBAL_ALL
--   fromCode 0 = CURL_GLOBAL_NOTHING
--   fromCode 4 = CURL_GLOBAL_ACK_EINTR
--   fromCode x = lie_idris_crash $ "Global flag was not a valid flag: " ++ show x

export
Show CurlECode where
  show = showEnum

export
Eq CurlECode where
  (==) = eqEnum

export
Ord CurlECode where
  compare = compareEnum

curlECodeEnumList : List Int
curlECodeEnumList = [0..96]

export
ToCode CurlECode where
  toCode = enumTo curlECodeEnumList

export
FromCode CurlECode where
  unsafeFromCode = unsafeEnumFrom curlECodeEnumList
  fromCode = enumFrom curlECodeEnumList


text:
import Control.Monad.State

data Tree a = Empty | Node (Tree a) a (Tree a)

testTree : Tree String
testTree =
    Node (Node (Node Empty "Jim" Empty) "Fred"
    (Node Empty "Sheila" Empty)) "Alice"
    (Node Empty "Bob" (Node Empty "Eve" Empty))

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = pure Empty
treeLabelWith (Node left val right) =
    do
        leftLabelled <- treeLabelWith left
        (this :: rest) <- get
        put rest
        rightLabelled <- treeLabelWith right
        pure (Node leftLabelled (this, val) rightLabelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = evalState (treeLabelWith tree) [1..]

countEmpty : Tree a -> State Nat ()
countEmpty Empty =
    do
        count <- get
        put (S count)
countEmpty (Node left val right) =
    do
        countEmpty left
        countEmpty right

countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty =
    do
        (empties, nodes) <- get
        put ((S empties), nodes)
countEmptyNode (Node left val right) =
    do
        countEmptyNode left
        (empties, nodes) <- get
        put (empties, (S nodes))
        countEmptyNode right


text:
module SqlDsl

import Data.Vect

--%access public export

data SqlType : Type where
  SqlInt : SqlType
  SqlBool : SqlType
  SqlString : SqlType

data SqlExpr : SqlType -> Type where
  IntC : Int -> SqlExpr SqlInt
  BoolC : Bool -> SqlExpr SqlBool
  StringC : String -> SqlExpr SqlString
  PlusC : SqlExpr SqlInt -> SqlExpr SqlInt -> SqlExpr SqlInt
  ConcatC : SqlExpr SqlString -> SqlExpr SqlString -> SqlExpr SqlString
  EqualC : SqlExpr a -> SqlExpr a -> SqlExpr SqlBool
  NotC : SqlExpr SqlBool -> SqlExpr SqlBool
  Field : {t : SqlType} -> (alias : String) -> (name : String) -> SqlExpr t

int : Int -> SqlExpr SqlInt
int x = IntC x

bool : Bool -> SqlExpr SqlBool
bool x = BoolC x

str : String -> SqlExpr SqlString
str x = StringC x

(==) : SqlExpr a -> SqlExpr a -> SqlExpr SqlBool
(==) x y = EqualC x y

data Tuple : {a : Type} -> (f : a -> Type) -> Vect n a -> Type where
  Nil : Tuple f []
  (::) : f t -> Tuple f ts -> Tuple f (t :: ts)

Table : {n : Nat} -> Type
Table {n} = (String, Vect n (String, SqlType))

index : (i : Fin k) -> Tuple f ts -> f (index i ts)
index FZ (x::xs) = x
index (FS j) (x::xs) = index j xs

get : (t : (String, SqlType)) -> {ts : Vect n (String, SqlType)} -> Tuple (\t => SqlExpr (snd t)) ts -> {auto p : Elem t ts} -> SqlExpr (snd t)
get t (x :: xs) {p = Here} = x
get t (x :: xs) {p = There p'} = get t {p = p'} xs

data SqlQuery : Vect n (String, SqlType) -> Type where
  From : (t : Table) -> SqlQuery (snd t)
  Product : SqlQuery ts -> SqlQuery ts' -> (Tuple (\t => SqlExpr (snd t)) ts -> Tuple (\t => SqlExpr (snd t)) ts' -> Tuple (\t => SqlExpr (snd t)) ts'') -> SqlQuery ts''
  Where : SqlQuery ts -> (Tuple (\t => SqlExpr (snd t)) ts -> SqlExpr SqlBool) -> SqlQuery ts
  Select : SqlQuery ts -> (Tuple (\t => SqlExpr (snd t)) ts -> Tuple (\t => SqlExpr (snd t)) ts') -> SqlQuery ts'

from : (t : Table) -> SqlQuery (snd t)
from t = From t

product : (Tuple (\t => SqlExpr (snd t)) ts -> Tuple (\t => SqlExpr (snd t)) ts' -> Tuple (\t => SqlExpr (snd t)) ts'') -> SqlQuery ts -> SqlQuery ts' -> SqlQuery ts''
product proj q1 q2 = Product q1 q2 proj

where' : (Tuple (\t => SqlExpr (snd t)) ts -> SqlExpr SqlBool) -> SqlQuery ts -> SqlQuery ts
where' pred query = Where query pred

select : (Tuple (\t => SqlExpr (snd t)) ts -> Tuple (\t => SqlExpr (snd t)) ts') -> SqlQuery ts -> SqlQuery ts'
select f query = Select query f

compileExpr : SqlExpr t -> String
compileExpr (IntC x) = show x
compileExpr (BoolC x) = show x
compileExpr (StringC x) = "\"" ++ x ++ "\""
compileExpr (PlusC x y) = "(" ++ compileExpr x ++ " + " ++ compileExpr y ++ ")"
compileExpr (ConcatC x y) = "(" ++ compileExpr x ++ " ++ " ++ compileExpr y ++ ")"
compileExpr (EqualC x y) = "(" ++ compileExpr x ++ " = " ++ compileExpr y ++ ")"
compileExpr (NotC x) = "NOT" ++ compileExpr x
compileExpr (Field alias name) = alias ++ "." ++ name

mapToTuple : String -> (ts : Vect n (String, SqlType)) -> Tuple (\t => SqlExpr (snd t)) ts
mapToTuple alias [] = []
mapToTuple alias ((name, t) :: ts) = Field {t = t} alias name :: mapToTuple alias ts

tupleToString : {ts : Vect n (String, SqlType)} -> Tuple (\t => SqlExpr (snd t)) ts -> String
tupleToString {ts = []} [] = ""
tupleToString {ts = [t]} [e] = compileExpr e ++ " AS " ++ fst t
tupleToString {ts = t :: ts} (e :: es) = compileExpr e ++ " AS " ++ fst t ++ ", " ++ tupleToString es

compile' : {ts : Vect n (String, SqlType)} -> SqlQuery ts -> Int -> (Int -> String -> String) -> String
compile' (Select {ts} (From (tableName, _)) f) i k =
  let alias = "c" ++ show i in
  let tuple' = f $ mapToTuple alias ts in
  let sql = "SELECT " ++ tupleToString tuple' ++ " FROM " ++ tableName ++ " AS " ++ alias in
  k (i + 1) sql
compile' (Select {ts} (Where (From (tableName, _)) pred) f) i k =
  let alias = "c" ++ show i in
  let tuple' = f $ mapToTuple alias ts in
  let sql = "SELECT " ++ tupleToString tuple' ++ " FROM " ++ tableName ++ " AS " ++ alias ++ " WHERE " ++ (compileExpr $ pred $ mapToTuple alias ts) in
  k (i + 1) sql
compile' (From (tableName, ts)) i k =
  let alias = "c" ++ show i in
  let sql = "SELECT * FROM " ++ tableName ++ " AS " ++ alias in
  k (i + 1) sql
compile' {ts} (Where query pred) i k =
  compile' query i (\i, sql =>
    let alias = "c" ++ show i in
    let sql' = "SELECT * FROM (" ++ sql ++ ") AS " ++ alias ++ " WHERE " ++ (compileExpr $ pred $ mapToTuple alias ts) in
    k (i + 1) sql')
compile' (Select {ts} query f) i k =
  compile' query i (\i, sql =>
    let alias = "c" ++ show i in
    let tuple' = f $ mapToTuple alias ts in
    let sql' = "SELECT " ++ tupleToString tuple' ++ " FROM (" ++ sql ++ ") AS " ++ alias in
    k (i + 1) sql')
compile' (Product {ts} {ts'} q1 q2 f) i k =
  compile' q1 i (\i, sql =>
    compile' q2 i (\i, sql' =>
      let alias = "c" ++ show i in
      let i' = i + 1 in
      let alias' = "c" ++ show i' in
      let tuple' = f (mapToTuple alias ts) (mapToTuple alias' ts') in
      let sql'' = "SELECT " ++ tupleToString tuple' ++ " FROM (" ++ sql ++ ") AS " ++ alias ++ ", (" ++ sql' ++ ") AS " ++ alias' in
      k (i' + 1) sql''))

compile : SqlQuery ts -> String
compile query = compile' query 0 (\_, sql => sql)

customer : Table {n = 3}
customer = ("Customer", [("Id", SqlInt),
                         ("Name", SqlString),
                         ("Age", SqlInt)])

--
example0 : SqlQuery [("Id", SqlInt), ("Name", SqlString), ("Age", SqlInt)]
example0 = from customer

example1 : SqlQuery [("Name", SqlString)]
example1 = select (\ta  => [get ("Name", SqlString) {ts = snd customer} ta]) $ from customer

example2 : SqlQuery [("Id", SqlInt)]
example2 = select (\ta => [index 0 ta]) $ from customer

example3 : SqlQuery [("Id", SqlInt), ("Age", SqlInt)]
example3 = select (\ta => [index 0 ta, index 2 ta]) $ where' (\ta => index 1 ta == str "Nick") $ from customer

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Data.Vect

%default total

{- Types can be treat in same way as the values. -}
returnType : Nat -> Type
returnType Z = Int
returnType (S Z) = String
returnType (S (S n)) = Int -> Int -> Int

{- We can return Int, String or function based on input value -}
valueType : (n : Nat) -> returnType n
valueType Z = 1
valueType (S Z) = "Hello World"
valueType (S (S n)) = \x => \y => x + y

{- Let's extend this idea to variable length input -}

variableType : (n : Nat) -> Type -> Type
variableType Z type = type
variableType (S k) type = type -> variableType k type

{- This function constructs a type level function
λΠ> variableType 0
variableType 0 : Type -> Type
λΠ> variableType 0 Int
Int : Type
λΠ> variableType 1 INT
When checking an application of function Main.variableType:
        No such variable INT
λΠ> variableType 1 Int
Int -> Int : Type
λΠ> variableType 2 Int
Int -> Int -> Int : Type
λΠ> variableType 3 String
String -> String -> String -> String : Type -}

variableValue : (n : Nat) -> (x : Type) -> (f : x -> x -> x) -> (y : x) ->  variableType n x
variableValue Z x f y = y
variableValue (S k) x f y = \inp => variableValue k x f (f inp y)

{-
λΠ> :t variableValue 0 Int (+)
variableValue 0 Int (+) : Int -> Int

λΠ> variableValue 1 Int (+) 2 3
5 : Int
λΠ> variableValue 1 String (++) "Hello" "World"
"WorldHello" : String
-}

{-
printf "Hello!" : String
printf "Answer: %d" : Int -> String
printf "%s number %d" : String -> Int -> String

-}

{-  This function does not work because of reduction problem,
    so try parsing string into AST -}
printfType : List Char  -> Type
printfType [] = String
printfType ('%' :: 'd' :: rest)  = Int -> printfType rest
printfType ('%' :: 's' :: rest) = String -> printfType rest
printfType (c :: rest)  = printfType rest

{- construct value level function -}
printfValue : (xs : List Char) -> String -> printfType xs
printfValue [] acc = acc
printfValue ('%' :: 'd' :: rest) acc = \x => printfValue rest (acc ++ show x)
printfValue ('%' :: 's' :: rest) acc = \x => printfValue rest (acc ++ x)
printfValue (c :: rest) acc = ?acc --  printfValue rest (acc ++ singleton c)

{- It works, but useless because last one is not reducing
λΠ> printfValue (unpack "%s%d%s") "" "hello" 2 "world"
"hello2world" : String
-}

data Format = FInt Format
            | FString Format
            | FOther Char Format
            | FEnd

format : List Char -> Format
format [] = FEnd
format ('%' :: 'd' :: cs ) = FInt (format cs)
format ('%' :: 's' :: cs ) = FString (format cs)
format (c :: cs)         = FOther c (format cs)

interpFormat : Format -> Type
interpFormat FEnd = String
interpFormat (FInt f)     = Int -> interpFormat f
interpFormat (FString f)  = String -> interpFormat f
interpFormat (FOther _ f) = interpFormat f

formatString : String -> Format
formatString s = format (unpack s)

toFunction : (fmt : Format) -> (acc : String) -> interpFormat fmt
toFunction FEnd acc = acc
toFunction (FInt f) acc     = \i => toFunction f (acc ++ show i)
toFunction (FString f) acc  = \s => toFunction f (acc ++ s)
toFunction (FOther c f) acc = toFunction f (acc ++ singleton c)

printf : (s : String) -> interpFormat (formatString s)
printf s = toFunction (formatString s) ""

{- Matrix with n rows and m column -}

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

repeat : (n : Nat) -> a -> Vect n a
repeat Z     _ = []
repeat (S n) a = a::repeat n a

transposeM : Matrix m n a -> Matrix n m a
transposeM []      = repeat _ []
transposeM (x::xs) = zipWith (::) x (transposeM xs)

twoByThree : Matrix 2 3 Int
twoByThree = [[1,2,3],
              [4,5,6]]

threeByTwo : Matrix 3 2 Int
threeByTwo = [[1, 4],
              [2, 5],
              [3, 6]]

tProof : (xs : Matrix n m a) -> transposeM (transposeM xs) = xs
tProof xs = ?proofisleftasanexercisetothereader

{- This code is literally copied from memory when I was learning Haskell -}
matrixMultiplication : Num a =>  Matrix m r a -> Matrix r n a -> Matrix m n a
matrixMultiplication xs ys = [[sum $ zipWith (*) ar bc | bc <- (transposeM ys)] | ar <- xs]

max_stars_repo_name: mukeshtiwari/CanberraFP

max_issues_repo_name: mukeshtiwari/CanberraFP

max_forks_repo_name: mukeshtiwari/CanberraFP


text:
module Data.Lawful.Eqv

%default total

||| `Eq` enriched with reflexivity, commutativity and transitivity.
public export
interface Eq a => Eqv a where
  0 eqvReflexive   : (x : a) -> x == x = True
  0 eqvCommutative : (x, y : a) -> x == y = y == x
  0 eqvTransitive  : (x, y, z : a) -> x == y = True -> y == z = True -> x == z = True

export
Eqv () where
  eqvReflexive () = Refl
  eqvCommutative () () = Refl
  eqvTransitive () () () Refl Refl = Refl

export
Eqv Bool where
  eqvReflexive True  = Refl
  eqvReflexive False = Refl

  eqvCommutative True  True  = Refl
  eqvCommutative True  False = Refl
  eqvCommutative False True  = Refl
  eqvCommutative False False = Refl

  eqvTransitive True  True  True  Refl Refl = Refl
  eqvTransitive False False False Refl Refl = Refl

export
Eqv Nat where
  eqvReflexive 0     = Refl
  eqvReflexive (S n) = rewrite eqvReflexive n in Refl

  eqvCommutative 0     0     = Refl
  eqvCommutative 0     (S m) = Refl
  eqvCommutative (S n) 0     = Refl
  eqvCommutative (S n) (S m) = rewrite eqvCommutative n m in Refl

  eqvTransitive Z Z Z Refl Refl = Refl
  eqvTransitive (S n) (S m) (S k) nm mk = eqvTransitive n m k nm mk

split_and : {a, b : Bool} -> a && b = True -> (a = True, b = True)
split_and {a=True} {b=True} Refl = (Refl, Refl)

export
Eqv a => Eqv (List a) where
  eqvReflexive [] = Refl
  eqvReflexive (x::xs) = rewrite eqvReflexive x in eqvReflexive xs

  eqvCommutative [] [] = Refl
  eqvCommutative [] (x::xs) = Refl
  eqvCommutative (x::xs) [] = Refl
  eqvCommutative (x::xs) (y::ys) = rewrite eqvCommutative x y in
                                   rewrite eqvCommutative xs ys in
                                   Refl

  eqvTransitive [] [] [] Refl Refl = Refl
  eqvTransitive (x::xs) (y::ys) (z::zs) xy yz = rewrite eqvTransitive x y z (fst $ split_and xy) (fst $ split_and yz) in
                                                rewrite eqvTransitive xs ys zs (snd $ split_and xy) (snd $ split_and yz) in
                                                Refl

export
(Eqv a, Eqv b) => Eqv (a, b) where
  eqvReflexive (a, b) = rewrite eqvReflexive a in
                        rewrite eqvReflexive b in
                        Refl

  eqvCommutative (a, b) (c, d) = rewrite eqvCommutative a c in
                                 rewrite eqvCommutative b d in
                                 Refl

  eqvTransitive (a, b) (c, d) (e, f) ac ce = rewrite eqvTransitive a c e (fst $ split_and ac) (fst $ split_and ce) in
                                             rewrite eqvTransitive b d f (snd $ split_and ac) (snd $ split_and ce) in
                                             Refl

export
(Eqv a, Eqv b) => Eqv (Either a b) where
  eqvReflexive (Left x)  = rewrite eqvReflexive x in Refl
  eqvReflexive (Right y) = rewrite eqvReflexive y in Refl

  eqvCommutative (Left x)  (Left y)  = rewrite eqvCommutative x y in Refl
  eqvCommutative (Right x) (Right y) = rewrite eqvCommutative x y in Refl
  eqvCommutative (Left x) (Right y) = Refl
  eqvCommutative (Right x) (Left y) = Refl

  eqvTransitive (Left x)  (Left y)  (Left z ) xy yz = eqvTransitive x y z xy yz
  eqvTransitive (Right x) (Right y) (Right z) xy yz = eqvTransitive x y z xy yz

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
Symmetric : {c : Type} -> (c -> c -> Type) -> Type
Symmetric {c} rel = {a : c} -> {b : c} -> rel a b -> rel b a

record Symmetry (t : Type) (rel : t -> t -> Type) where
  constructor MkSymmetry
  is_symmetric : Symmetric {c=t} rel

symmetry : {ty : Type} -> Symmetry ty (=)
symmetry = MkSymmetry sym

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Network.HTTP.Message

import Data.String.Parser
import Data.String.Extra
import Generics.Derive
import Network.HTTP.Header
import Network.HTTP.Status
import Network.HTTP.Method

import Debug.Trace

%language ElabReflection

public export
RawHeaders : Type
RawHeaders = List (String, String)

public export
record RawHttpMessage where
  constructor MkRawHttpMessage
  method : Method
  path : String
  headers : RawHeaders

public export
record HttpResponse where
  constructor MkHttpResponse
  status_code : (n ** StatusCode n)
  status_name : String
  headers : RawHeaders

%runElab derive "RawHttpMessage" [Generic, Meta, Show]
%runElab derive "HttpResponse" [Generic, Meta, Show]

export
serialize_http_message : RawHttpMessage -> String
serialize_http_message message =
  join "\r\n"
  $ [ http_method_to_string message.method <+> " " <+> message.path <+> " HTTP/1.1" ]
  <+> map (\(k,v) => "\{k}: \{v}") message.headers
  <+> [ "", "" ]

export
serialize_http_response : HttpResponse -> String
serialize_http_response response =
  join "\r\n"
  $ [ "HTTP/1.1 " <+> show (response.status_code.fst) <+> response.status_name ]
  <+> map (\(k,v) => "\{k}: \{v}") response.headers
  <+> [ "", "" ]

eol : Monad m => ParseT m ()
eol = (string "\r\n" <|> string "\n") $> ()

is_eol : Char -> Bool
is_eol '\r' = True
is_eol '\n' = True
is_eol _ = False

header : Parser (String, String)
header = do
  key <- takeUntil ":"
  value <- takeWhile1 (not . is_eol)
  eol
  pure (key, (ltrim value))

export
http_message_praser : Parser RawHttpMessage
http_message_praser = do
  method <- string_to_http_method . pack <$> some (satisfy isUpper)
  _ <- char ' '
  path <- takeUntil " "
  _ <- string "HTTP/1.1"
  eol
  headers <- many header
  eol
  pure (MkRawHttpMessage method path headers)

export
deserialize_http_message : String -> Either String RawHttpMessage
deserialize_http_message = map fst . parse http_message_praser

export
http_message_response : Parser HttpResponse
http_message_response = do
  _ <- many eol
  _ <- string "HTTP/1.1 " <|> string "HTTP/1.0 "
  status_code <- natural
  _ <- char ' '
  status_name <- takeWhile1 (not . is_eol)
  eol
  headers <- many header
  case is_status_code_number status_code of
    Yes ok => pure (MkHttpResponse (status_code ** nat_to_status_code status_code ok) status_name headers)
    No _ => fail $ "status code " <+> show status_code <+> " is outside of bound"

export
deserialize_http_response : String -> Either String HttpResponse
deserialize_http_response = map fst . parse http_message_response


text:
module TTImp.Elab.Ambiguity

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

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp

import Data.List
import Data.String

import Libraries.Data.UserNameMap

%default covering

export
expandAmbigName : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto e : Ref EST (EState vars)} ->
                  ElabMode -> NestedNames vars -> Env Term vars -> RawImp ->
                  List (FC, Maybe (Maybe Name), RawImp) ->
                  RawImp -> Maybe (Glued vars) -> Core RawImp
expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp
    = do est <- get EST
         if UN (Basic n) `elem` lhsPatVars est
            then pure $ IMustUnify fc NonLinearVar orig
            else pure $ orig
expandAmbigName mode nest env orig args (IVar fc x) exp
   = case lookup x (names nest) of
          Just _ => do log "elab.ambiguous" 10 $ "Nested " ++ show x
                       pure orig
          Nothing => do
             defs <- get Ctxt
             case defined x env of
                  Just _ =>
                    if isNil args || notLHS mode
                       then do log "elab.ambiguous" 10 $ "Defined in env " ++ show x
                               pure $ orig
                       else pure $ IMustUnify fc VarApplied orig
                  Nothing =>
                     do est <- get EST
                        primNs <- getPrimNames
                        let prims = primNamesToList primNs
                        let primApp = isPrimName prims x
                        case lookupUN (userNameRoot x) (unambiguousNames est) of
                          Just xr => do
                            log "elab.ambiguous" 10 $ "unambiguous: " ++ show (fst xr)
                            pure $ mkAlt primApp est xr
                          Nothing => do
                            ns <- lookupCtxtName x (gamma defs)
                            ns' <- filterM visible ns
                            case ns' of
                               [] => do log "elab.ambiguous" 10 $ "Failed to find " ++ show orig
                                        pure orig
                               [nalt] =>
                                     do log "elab.ambiguous" 10 $ "Only one " ++ show (fst nalt)
                                        pure $ mkAlt primApp est nalt
                               nalts => pure $ IAlternative fc
                                                      (uniqType primNs x args)
                                                      (map (mkAlt primApp est) nalts)
  where
    lookupUN : Maybe UserName -> UserNameMap a -> Maybe a
    lookupUN Nothing _ = Nothing
    lookupUN (Just n) sm = lookup n sm

    visible : (Name, Int, GlobalDef) -> Core Bool
    visible (n, i, def)
        = do let NS ns x = fullname def
                 | _ => pure True
             if !(isVisible ns)
                then pure $ visibleInAny (!getNS :: !getNestedNS) (NS ns x)
                                         (visibility def)
                else pure False

    -- If there's multiple alternatives and all else fails, resort to using
    -- the primitive directly
    uniqType : PrimNames -> Name -> List (FC, Maybe (Maybe Name), RawImp) -> AltType
    uniqType (MkPrimNs (Just fi) _ _ _) n [(_, _, IPrimVal fc (BI x))]
        = UniqueDefault (IPrimVal fc (BI x))
    uniqType (MkPrimNs _ (Just si) _ _) n [(_, _, IPrimVal fc (Str x))]
        = UniqueDefault (IPrimVal fc (Str x))
    uniqType (MkPrimNs _ _ (Just ci) _) n [(_, _, IPrimVal fc (Ch x))]
        = UniqueDefault (IPrimVal fc (Ch x))
    uniqType (MkPrimNs _ _ _ (Just di)) n [(_, _, IPrimVal fc (Db x))]
        = UniqueDefault (IPrimVal fc (Db x))
    uniqType _ _ _ = Unique

    buildAlt : RawImp -> List (FC, Maybe (Maybe Name), RawImp) ->
               RawImp
    buildAlt f [] = f
    buildAlt f ((fc', Nothing, a) :: as)
        = buildAlt (IApp fc' f a) as
    buildAlt f ((fc', Just Nothing, a) :: as)
        = buildAlt (IAutoApp fc' f a) as
    buildAlt f ((fc', Just (Just i), a) :: as)
        = buildAlt (INamedApp fc' f i a) as

    -- If it's not a constructor application, dot it
    wrapDot : Bool -> EState vars ->
              ElabMode -> Name -> List RawImp -> Def -> RawImp -> RawImp
    wrapDot _ _ _ _ _ (DCon _ _ _) tm = tm
    wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _ _ _) tm = tm
    -- Leave primitive applications alone, because they'll be inlined
    -- before compiling the case tree
    wrapDot prim est (InLHS _) n' [arg] _ tm
       = if n' == Resolved (defining est) || prim
            then tm
            else IMustUnify fc NotConstructor tm
    wrapDot prim est (InLHS _) n' _ _ tm
       = if n' == Resolved (defining est)
            then tm
            else IMustUnify fc NotConstructor tm
    wrapDot _ _ _ _ _ _ tm = tm

    mkTerm : Bool -> EState vars -> Name -> GlobalDef -> RawImp
    mkTerm prim est n def
        = let tm = wrapDot prim est mode n (map (snd . snd) args)
                       (definition def) (buildAlt (IVar fc n) args) in
              if Macro `elem` flags def
                 then case mode of
                           InLHS _ => tm
                           _ => IRunElab fc (ICoerced fc tm)
                 else tm

    mkAlt : Bool -> EState vars -> (Name, Int, GlobalDef) -> RawImp
    mkAlt prim est (fullname, i, gdef)
        = mkTerm prim est (Resolved i) gdef

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

expandAmbigName mode nest env orig args (IApp fc f a) exp
    = expandAmbigName mode nest env orig
                      ((fc, Nothing, a) :: args) f exp
expandAmbigName mode nest env orig args (INamedApp fc f n a) exp
    = expandAmbigName mode nest env orig
                      ((fc, Just (Just n), a) :: args) f exp
expandAmbigName mode nest env orig args (IAutoApp fc f a) exp
    = expandAmbigName mode nest env orig
                      ((fc, Just Nothing, a) :: args) f exp
expandAmbigName elabmode nest env orig args tm exp
    = do log "elab.ambiguous" 10 $ "No ambiguity " ++ show orig
         pure orig

stripDelay : NF vars -> NF vars
stripDelay (NDelayed fc r t) = stripDelay t
stripDelay tm = tm

data TypeMatch = Concrete | Poly | NoMatch

Show TypeMatch where
  show Concrete = "Concrete"
  show Poly = "Poly"
  show NoMatch = "NoMatch"

mutual
  mightMatchD : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Defs -> NF vars -> NF [] -> Core TypeMatch
  mightMatchD defs l r
      = mightMatch defs (stripDelay l) (stripDelay r)

  mightMatchArg : {auto c : Ref Ctxt Defs} ->
                  {vars : _} ->
                  Defs ->
                  Closure vars -> Closure [] ->
                  Core Bool
  mightMatchArg defs l r
      = pure $ case !(mightMatchD defs !(evalClosure defs l) !(evalClosure defs r)) of
             NoMatch => False
             _ => True

  mightMatchArgs : {auto c : Ref Ctxt Defs} ->
                   {vars : _} ->
                   Defs ->
                   List (Closure vars) -> List (Closure []) ->
                   Core Bool
  mightMatchArgs defs [] [] = pure True
  mightMatchArgs defs (x :: xs) (y :: ys)
      = do amatch <- mightMatchArg defs x y
           if amatch
              then mightMatchArgs defs xs ys
              else pure False
  mightMatchArgs _ _ _ = pure False

  mightMatch : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Defs -> NF vars -> NF [] -> Core TypeMatch
  mightMatch defs target (NBind fc n (Pi _ _ _ _) sc)
      = mightMatchD defs target !(sc defs (toClosure defaultOpts [] (Erased fc False)))
  mightMatch defs (NBind _ _ _ _) (NBind _ _ _ _) = pure Poly -- lambdas might match
  mightMatch defs (NTCon _ n t a args) (NTCon _ n' t' a' args')
      = if n == n'
           then do amatch <- mightMatchArgs defs (map snd args) (map snd args')
                   if amatch then pure Concrete else pure NoMatch
           else pure NoMatch
  mightMatch defs (NDCon _ n t a args) (NDCon _ n' t' a' args')
      = if t == t'
           then do amatch <- mightMatchArgs defs (map snd args) (map snd args')
                   if amatch then pure Concrete else pure NoMatch
           else pure NoMatch
  mightMatch defs (NPrimVal _ x) (NPrimVal _ y)
      = if x == y then pure Concrete else pure NoMatch
  mightMatch defs (NType _) (NType _) = pure Concrete
  mightMatch defs (NApp _ _ _) _ = pure Poly
  mightMatch defs (NErased _ _) _ = pure Poly
  mightMatch defs _ (NApp _ _ _) = pure Poly
  mightMatch defs _ (NErased _ _) = pure Poly
  mightMatch _ _ _ = pure NoMatch

-- Return true if the given name could return something of the given target type
couldBeName : {auto c : Ref Ctxt Defs} ->
              {vars : _} ->
              Defs -> NF vars -> Name -> Core TypeMatch
couldBeName defs target n
    = case !(lookupTyExact n (gamma defs)) of
           Nothing => pure Poly -- could be a local name, don't rule it out
           Just ty => mightMatchD defs target !(nf defs [] ty)

couldBeFn : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Defs -> NF vars -> RawImp -> Core TypeMatch
couldBeFn defs ty (IVar _ n) = couldBeName defs ty n
couldBeFn defs ty (IAlternative _ _ _) = pure Concrete
couldBeFn defs ty _ = pure Poly

-- Returns Nothing if there's no possibility the expression's type matches
-- the target type
-- Just (True, app) if it's a match on concrete return type
-- Just (False, app) if it might be a match due to being polymorphic
couldBe : {auto c : Ref Ctxt Defs} ->
          {vars : _} ->
          Defs -> NF vars -> RawImp -> Core (Maybe (Bool, RawImp))
couldBe {vars} defs ty@(NTCon _ n _ _ _) app
   = case !(couldBeFn {vars} defs ty (getFn app)) of
          Concrete => pure $ Just (True, app)
          Poly => pure $ Just (False, app)
          NoMatch => pure Nothing
couldBe {vars} defs ty@(NPrimVal _ _) app
   = case !(couldBeFn {vars} defs ty (getFn app)) of
          Concrete => pure $ Just (True, app)
          Poly => pure $ Just (False, app)
          NoMatch => pure Nothing
couldBe {vars} defs ty@(NType _) app
   = case !(couldBeFn {vars} defs ty (getFn app)) of
          Concrete => pure $ Just (True, app)
          Poly => pure $ Just (False, app)
          NoMatch => pure Nothing
couldBe defs ty app = pure $ Just (False, app)

notOverloadable : Defs -> (Bool, RawImp) -> Core Bool
notOverloadable defs (True, fn) = pure True
notOverloadable defs (concrete, fn) = notOverloadableFn (getFn fn)
  where
    notOverloadableFn : RawImp -> Core Bool
    notOverloadableFn (IVar _ n)
        = do Just gdef <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure True
             pure False -- If the name exists, and doesn't have a concrete type
                        -- but another possibility does, remove it from the set
                        -- no matter what
                        -- (TODO: Consider whether %allow_overloads should exist)
                        -- (not (Overloadable `elem` flags gdef))
    notOverloadableFn _ = pure True

filterCore : (a -> Core Bool) -> List a -> Core (List a)
filterCore f [] = pure []
filterCore f (x :: xs)
    = do p <- f x
         xs' <- filterCore f xs
         if p then pure (x :: xs')
              else pure xs'

pruneByType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              Env Term vars -> NF vars -> List RawImp ->
              Core (List RawImp)
pruneByType env target alts
    = do defs <- get Ctxt
         matches_in <- traverse (couldBe defs (stripDelay target)) alts
         let matches = mapMaybe id matches_in
         logNF "elab.prune" 10 "Prune by" env target
         log "elab.prune" 10 (show matches)
         res <- if any Builtin.fst matches
                -- if there's any concrete matches, drop the non-concrete
                -- matches marked as '%allow_overloads' from the possible set
                   then do keep <- filterCore (notOverloadable defs) matches
                           log "elab.prune" 10 $ "Keep " ++ show keep
                           pure (map snd keep)
                   else pure (map snd matches)
         if isNil res
            then pure alts -- if none of them work, better to show all the errors
            else pure res

checkAmbigDepth : {auto c : Ref Ctxt Defs} ->
                  {auto e : Ref EST (EState vars)} ->
                  FC -> ElabInfo -> Core ()
checkAmbigDepth fc info
    = do max <- getAmbigLimit
         let ambs = ambigTries info
         when (length ambs > max) $
           do est <- get EST
              throw (AmbiguityTooDeep fc (Resolved (defining est)) ambs)

getName : RawImp -> Maybe Name
getName (IVar _ n) = Just n
getName (IApp _ f _) = getName f
getName (INamedApp _ f _ _) = getName f
getName (IAutoApp _ f _) = getName f
getName _ = Nothing

export
addAmbig : List alts -> Maybe Name -> ElabInfo -> ElabInfo
addAmbig _ Nothing = id
addAmbig [] _ = id
addAmbig [_] _ = id
addAmbig _ (Just n) = record { ambigTries $= (n ::) }

export
checkAlternative : {vars : _} ->
                   {auto c : Ref Ctxt Defs} ->
                   {auto m : Ref MD Metadata} ->
                   {auto u : Ref UST UState} ->
                   {auto e : Ref EST (EState vars)} ->
                   RigCount -> ElabInfo ->
                   NestedNames vars -> Env Term vars ->
                   FC -> AltType -> List RawImp -> Maybe (Glued vars) ->
                   Core (Term vars, Glued vars)
checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
    = do checkAmbigDepth fc elabinfo
         expected <- maybe (do nm <- genName "altTy"
                               ty <- metaVar fc erased env nm (TType fc)
                               pure (gnf env ty))
                           pure mexpected
         let solvemode = case elabMode elabinfo of
                              InLHS c => inLHS
                              _ => inTerm
         delayOnFailure fc rig env (Just expected) ambiguous Ambiguity $
             \delayed =>
               do solveConstraints solvemode Normal
                  defs <- get Ctxt
                  exp <- getTerm expected

                  -- We can't just use the old NF on the second attempt,
                  -- because we might know more now, so recalculate it
                  let exp' = if delayed
                                then gnf env exp
                                else expected

                  logGlueNF "elab.ambiguous" 5 (fastConcat
                    [ "Ambiguous elaboration at ", show fc, ":\n"
                    , unlines (map show alts)
                    , "With default. Target type "
                    ]) env exp'
                  alts' <- pruneByType env !(getNF exp') alts
                  log "elab.prune" 5 $
                    "Pruned " ++ show (minus (length alts) (length alts')) ++ " alts."
                    ++ " Kept:\n" ++ unlines (map show alts')

                  if delayed -- use the default if there's still ambiguity
                     then try
                            (exactlyOne' False fc env
                                (map (\t =>
                                   (getName t,
                                    checkImp rig (addAmbig alts' (getName t) elabinfo)
                                             nest env t
                                             (Just exp'))) alts'))
                            (do log "elab.ambiguous" 5 "All failed, running default"
                                checkImp rig (addAmbig alts' (getName def) elabinfo)
                                             nest env def (Just exp'))
                     else exactlyOne' True fc env
                           (map (\t =>
                             (getName t,
                              checkImp rig (addAmbig alts' (getName t) elabinfo)
                                       nest env t (Just exp')))
                              alts')
checkAlternative rig elabinfo nest env fc uniq alts mexpected
    = do checkAmbigDepth fc elabinfo
         alts' <- maybe (Core.pure [])
                        (\exp => pruneByType env !(getNF exp) alts) mexpected
         case alts' of
           [alt] => checkImp rig elabinfo nest env alt mexpected
           _ =>
             do expected <- maybe (do nm <- genName "altTy"
                                      ty <- metaVar fc erased env nm (TType fc)
                                      pure (gnf env ty))
                                  pure mexpected
                let solvemode = case elabMode elabinfo of
                                      InLHS c => inLHS
                                      _ => inTerm
                delayOnFailure fc rig env (Just expected) ambiguous Ambiguity $
                     \delayed =>
                       do defs <- get Ctxt
                          exp <- getTerm expected

                          -- We can't just use the old NF on the second attempt,
                          -- because we might know more now, so recalculate it
                          let exp' = if delayed
                                        then gnf env exp
                                        else expected

                          alts' <- pruneByType env !(getNF exp') alts

                          logGlueNF "elab.ambiguous" 5 (fastConcat
                              [ "Ambiguous elaboration"
                              , " (kept ", show (length alts'), " out of "
                              , show (length alts), " candidates)"
                              , " (", if delayed then "" else "not ", "delayed)"
                              , " at ", show fc, ":\n"
                              , unlines (map show alts')
                              , "Target type "
                              ]) env exp'
                          let tryall = case uniq of
                                            FirstSuccess => anyOne fc
                                            _ => exactlyOne' (not delayed) fc env
                          tryall (map (\t =>
                              (getName t,
                               do res <- checkImp rig (addAmbig alts' (getName t) elabinfo)
                                                  nest env t (Just exp')
                                  -- Do it twice for interface resolution;
                                  -- first pass gets the determining argument
                                  -- (maybe rethink this, there should be a better
                                  -- way that allows one pass)
                                  solveConstraints solvemode Normal
                                  solveConstraints solvemode Normal
                                  log "elab.ambiguous" 10 $ show (getName t) ++ " success"
                                  pure res)) alts')