text:
module Primes

import NatUtils
import gcd
import NatOrder

%access public export
%default total

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- creates a list with all the factors of a number upto the second arguement
genFact : (n : Nat) -> Nat -> List (k : Nat ** isDivisible n k)
genFact Z Z = []
genFact Z (S k) = []
genFact (S j) Z = []
genFact (S Z) (S k) = [(S Z ** oneDiv (S Z))]
genFact (S (S j)) (S k) =
    case (decDiv (S (S j)) (LTESucc (LTESucc (LTEZero{right = j}))) (S k)
          {euc=euclidDivide (S (S j)) (S k) SIsNotZ }) of
               (Yes prf) => (genFact (S (S j)) k) ++ [(S k ** prf)]
               (No contra) => (genFact (S (S j)) k)

--if the List has only 2 elements, i.e 1 and p, then the number is prime. the function outputs a list (secretly genFact)
-- along with the proof that the length of the list of factors is 2
isPrimeWithoutProof : (p: Nat) -> {auto pf: LTE 2 p} -> Type
isPrimeWithoutProof p = length (genFact p p) = 2

-- more than 2 factors implies number is composite
isCompositeWithoutProof : (n: Nat) -> {auto pf: LTE 2 n} -> Type
isCompositeWithoutProof n = Prelude.Nat.GT (Prelude.List.length (genFact n n)) 2

--prime proof
isPrime : (p : Nat) -> LTE 2 p -> Type
isPrime p proofLTE = {k : Nat} -> isDivisible p k -> Either (k=1)(k=p)

-- Two is a prime
twoPr : (isPrime 2 (LTESucc (LTESucc (LTEZero {right =0}))))
twoPr {k=Z} (x ** pf) = void (SIsNotZ (snd pf))
twoPr {k=(S Z)} (x ** pf) = Left Refl
twoPr {k=(S (S Z))} (x ** pf) = Right Refl
twoPr {k=(S (S (S k)))} pf = void (bGtAImpNotbDivA 2 (S (S (S k))) k (LTESucc (LTESucc (LTESucc (LTEZero {right = k})))) (pf))

--Composite proof
isComposite : (n : Nat) -> LTE 2 n -> Type
isComposite n pflte = (a : Nat ** (b : Nat ** ((GT a 1, GT b 1), n = a*b)))

--deciability for Composite numbers
decComposite : (n: Nat) -> (pf : LTE 2 n) -> Dec (isComposite n pf)
decComposite Z LTEZero impossible
decComposite Z (LTESucc _) impossible
decComposite (S Z) (LTESucc LTEZero) impossible
decComposite (S Z) (LTESucc (LTESucc _)) impossible
decComposite (S (S k)) pf = ?decCompositerhs_1

--if 1<n, a not equal to a*n
aNotEqToMultA : (a : Nat) -> LTE 1 a -> (n : Nat) -> LTE 2 n -> (a = a*n) -> Void
aNotEqToMultA _ _ Z LTEZero _ impossible
aNotEqToMultA _ _ Z (LTESucc _) _ impossible
aNotEqToMultA _ _ (S Z) (LTESucc LTEZero) _ impossible
aNotEqToMultA _ _ (S Z) (LTESucc (LTESucc _)) _ impossible
aNotEqToMultA Z LTEZero (S (S _)) _ _ impossible
aNotEqToMultA Z (LTESucc _) (S (S _)) _ _ impossible
aNotEqToMultA (S j) (LTESucc (LTEZero {right = j})) (S (S k)) (LTESucc (LTESucc (LTEZero {right = k}))) prf =
                              SIsNotZ {x = j+(k*(S j))} (sym (pfeq)) where
                                pfeq  = plusLeftCancel (S j) Z ((S k)*(S j)) pfeq1 where
                                  pfeq1 = rewrite (multCommutative (S (S k)) (S j)) in
                                          trans (plusZeroRightNeutral (S j)) prf

--helper apNat function
apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

--n is not both prime and composite
notBothPrimeandComp : {n : Nat} -> (pf : LTE 2 n) -> Not (isPrime n pf, isComposite n pf)
notBothPrimeandComp {n = Z} LTEZero _ impossible
notBothPrimeandComp {n = Z} (LTESucc _) _ impossible
notBothPrimeandComp {n = (S Z)} (LTESucc LTEZero) _ impossible
notBothPrimeandComp {n = (S Z)} (LTESucc (LTESucc _)) _ impossible
notBothPrimeandComp {n = (S (S k))} pftwolten (pfprime , (a ** (b ** ((pfagtone, pfbgtone), pfneqab)))) =
                            void (aNotEqToMultA (S (S k)) (lteTransitive (LTESucc (LTEZero {right = (S Z)})) pftwolten) b pfbgtone pfeq) where
                              pfeq = (trans pfneqab funceq) where
                                funceq = (apNat (\x=>(x*b)) a (S (S k)) pfaeqn) where
                                  pfaeqn =  case (pfprime (b ** ((lteTransitive (LTESucc (LTEZero {right = (S Z)})) pfbgtone), pfneqab))) of
                                          Left pf => void ((Prelude.Basics.fst (ltImpliesNotEqNotGT {a=(S Z)} {b = a} pfagtone)) (sym pf))
                                          Right pf => pf

-- given n >= 2, it is either prime or Composite
eitherPrimeOrComp : {n : Nat} -> (pf : LTE 2 n) -> Either (isPrime n pf)(isComposite n pf)
eitherPrimeOrComp {n = Z} LTEZero impossible
eitherPrimeOrComp {n = Z} (LTESucc _) impossible
eitherPrimeOrComp {n = (S Z)} (LTESucc LTEZero) impossible
eitherPrimeOrComp {n = (S Z)} (LTESucc (LTESucc _)) impossible
eitherPrimeOrComp {n = (S (S k))} pflte = ?rhs_1

  -- data Prime : (p : Nat) -> Type where
  --  IsPrime : LTE 2 p -> ((k : Nat) -> isDivisible p k -> Either (k=1)(k=p)) -> Prime p

  -- function to check that 2 is prime
  -- twoPr : (k : Nat) -> (isDivisible 2 k) -> Either (k = 1)(k = 2)
  -- twoPr Z (x ** pf) = void (SIsNotZ (snd pf))
  -- twoPr (S Z) (x ** pf) = Left Refl
  -- twoPr (S (S Z)) (x ** pf) = Right Refl
  -- twoPr (S (S (S k))) pf = void (bGtAImpNotbDivA 2 (S (S (S k))) k (LTESucc (LTESucc (LTESucc (LTEZero {right = k})))) (pf))
  --
  -- --two is Prime
  -- twoIsPrime : Prime 2
  -- twoIsPrime = IsPrime (LTESucc (LTESucc (LTEZero {right =0}))) twoPr

-- notBothPrimeandComp Z LTEZero _ _ impossible
-- notBothPrimeandComp Z (LTESucc _) _ _ impossible
-- notBothPrimeandComp (S Z) (LTESucc LTEZero) _ _ impossible
-- notBothPrimeandComp (S Z) (LTESucc (LTESucc _)) _ _ impossible
-- notBothPrimeandComp (S (S k)) pfgt pfprime pfcomp = ?jk

--same as oneDiv, but fits the format for the following functions
-- oneIsFactor : (n : Nat) -> (LTE 1 n) -> (fromMaybe 0 (head' (List Nat)) = (S Z))
-- oneIsFactor Z LTEZero impossible
-- oneIsFactor Z (LTESucc _) impossible
-- oneIsFactor (S k) pf =
--
-- -- n is the last element of the list of its factors
-- nIsFactor : (n : Nat) -> (LTE 1 n) -> (fromMaybe 0 (tail' (genFact n n)) = n)
-- nIsFactor Z LTEZero impossible
-- nIsFactor Z (LTESucc _) impossible
-- nIsFactor (S k) pf = Refl

--Spare code
{-
--Type for isPrime. A number p is prime if all numbers dividing
--it are either p or 1. (In the primality checker, I am checking
--for numbers until p, hence the p case is not included. Will
--be changed in a future update.)
isPrime : Nat -> Type
isPrime p = (LTE 2 p ,
            (x : Nat **
            (isDivisible p x , x = 1)))
--Does the job, but is not very useful. Will be replaced later.
checkPrime : (p : Nat) -> LTE 2 p -> {default (p-1) iter : Nat} ->
  Maybe (isPrime p)
checkPrime p pf {iter=Z} = Nothing
checkPrime p pf {iter=(S Z)} = Just (pf, ((S Z) ** (oneDiv p, Refl)))
checkPrime p pf {iter=(S k)} = case modNatNZ p (S k) SIsNotZ of
                            Z => Nothing
                            (S m) => checkPrime p pf {iter=k}
-}


text:
import Data.Vect

||| Test if the type of local variables in do-notation is correctly reported

partial
f : Maybe Nat -> Nat -> Maybe Nat
f x y = do
    -- Bind
    x' <- x

    -- Pattern matching bind
    (S x'') <- x

    -- Let in Do
    let y' = y

    -- Let in Do with pattern matching
    let (S y'') = y

    -- Let in Do with signature
    let a : Nat
        a = x'

    -- Make sure the variable works regardless of how it was bound
    ?result x x' x'' y y' y'' a

ext: idr


text:
module StringLiterals

hello : FromString a => a
hello = "Hello"

helloName : String -> String
helloName name = "\{hello {a = String}} \{name}"

welcomeName : String -> String
welcomeName name = """
  \{helloName name}
  and welcome!
  """

scareQuotes : String
scareQuotes = #""hello""#

test : StringLiterals.scareQuotes = "\"hello\""
test = Refl


text:
module Html

import Js.VirtualDom
import Js.Utils

%include JavaScript "js/html.js"

public export
Html : Type -> Type
Html a = Node 'Html a

export
interface HtmlAllAttribute (o : Type) where

public export
HtmlAttribute : Type -> Type
HtmlAttribute a = Attribute 'HtmlAttribute a

public export
InputAttribute : Type -> Type
InputAttribute a = Attribute 'InputAttribute a

export
implementation HtmlAllAttribute 'HtmlAttribute where

export
implementation  HtmlAllAttribute 'InputAttribute where

-------- Nodes --------

export
div : List (HtmlAttribute a) -> List (Html a) -> Html a
div = node "div"

export
span : List (HtmlAttribute a) -> List (Html a) -> Html a
span = node "span"

export
emptySpan : Html a
emptySpan = span [] []

export
input : List (InputAttribute a) -> Html a
input attrs = node "input" attrs []

export
form : List (HtmlAttribute a) -> a -> List (Html a) -> Html a
form attrs val childs =
  node
  "form"
  (eventListenerAttributePreventDefault "submit" (\_ => pure val) :: attrs)
  childs

export
button : List (HtmlAttribute a) -> String -> Html a
button attrs txt = node "button" attrs [text txt]

export
img : List (HtmlAttribute a) -> String -> Html a
img attrs url =
  node
    "img"
    (stringAttribute "src" url :: attrs)
    []

-------- Attributes --------

export
value : String -> Attribute 'InputAttribute a
value v = propertyAttribute "value" v

export
cssClass : HtmlAllAttribute o => String -> Attribute o a
cssClass s = stringAttribute "class" s

-------- Events --------

export
onclick : HtmlAllAttribute o => a -> Attribute o a
onclick x = eventListenerAttribute "click" (\_ => pure x)

export
onchange : (String -> a) -> Attribute 'InputAttribute a
onchange convert =
  eventListenerAttribute
  "change"
  (\x => convert <$> jscall "%0.target.value" (Ptr -> JS_IO String) x)

export
onlongpress : HtmlAllAttribute o => a -> Attribute o a
onlongpress x = customEventListenerAttribute "longpress" (jscall "$JSLIB$html.addLongPressEventListener(%0)" (Ptr -> JS_IO ())) (\_ => pure x)

export
onshortpress : HtmlAllAttribute o => a -> Attribute o a
onshortpress x = customEventListenerAttribute "shortpress" (jscall "$JSLIB$html.addShortPressEventListener(%0)" (Ptr -> JS_IO ())) (\_ => pure x)

max_stars_repo_name: banyan-infrastructure/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module TTImp.Elab.Check
-- Interface (or, rather, type declaration) for the main checker function,
-- used by the checkers for each construct. Also some utility functions for
-- reading and writing elaboration state

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

import TTImp.TTImp

import Data.Either
import Libraries.Data.IntMap
import Data.List
import Libraries.Data.NameMap
import Libraries.Data.UserNameMap

%default covering

public export
data ElabMode = InType | InLHS RigCount | InExpr | InTransform

export
isLHS : ElabMode -> Maybe RigCount
isLHS (InLHS w) = Just w
isLHS _ = Nothing

Show ElabMode where
  show InType = "InType"
  show (InLHS c) = "InLHS " ++ show c
  show InExpr = "InExpr"
  show InTransform = "InTransform"

public export
data ElabOpt
  = HolesOkay
  | InCase
  | InPartialEval
  | InTrans

public export
Eq ElabOpt where
  HolesOkay == HolesOkay = True
  InCase == InCase = True
  InPartialEval == InPartialEval = True
  InTrans == InTrans = True
  _ == _ = False

-- Descriptions of implicit name bindings. They're either just the name,
-- or a binding of an @-pattern which has an associated pattern.
public export
data ImplBinding : List Name -> Type where
     NameBinding : {vars : _} ->
                   RigCount -> PiInfo (Term vars) -> (elabAs : Term vars) -> (expTy : Term vars) ->
                   ImplBinding vars
     AsBinding : {vars : _} ->
                 RigCount -> PiInfo (Term vars) -> (elabAs : Term vars) -> (expTy : Term vars) ->
                 (pat : Term vars) ->
                 ImplBinding vars

export
Show (ImplBinding vars) where
  show (NameBinding c p tm ty) = show (tm, ty)
  show (AsBinding c p tm ty pat) = show (tm, ty) ++ "@" ++ show tm

export
bindingMetas : ImplBinding vars -> NameMap Bool
bindingMetas (NameBinding c p tm ty) = getMetas ty
bindingMetas (AsBinding c p tm ty pat)
    = insertAll (toList (getMetas ty)) (getMetas pat)
  where
    insertAll : List (Name, Bool) -> NameMap Bool -> NameMap Bool
    insertAll [] ns = ns
    insertAll ((k, v) :: ks) ns = insert k v (insertAll ks ns)

-- Get the type of an implicit name binding
export
bindingType : ImplBinding vars -> Term vars
bindingType (NameBinding _ _ _ ty) = ty
bindingType (AsBinding _ _ _ ty _) = ty

-- Get the term (that is, the expanded thing it elaborates to, of the name
-- applied to the context) from an implicit binding
export
bindingTerm : ImplBinding vars -> Term vars
bindingTerm (NameBinding _ _ tm _) = tm
bindingTerm (AsBinding _ _ tm _ _) = tm

export
bindingRig : ImplBinding vars -> RigCount
bindingRig (NameBinding c _ _ _) = c
bindingRig (AsBinding c _ _ _ _) = c

export
bindingPiInfo : ImplBinding vars -> PiInfo (Term vars)
bindingPiInfo (NameBinding _ p _ _) = p
bindingPiInfo (AsBinding _ p _ _ _) = p

-- Current elaboration state (preserved/updated throughout elaboration)
public export
record EState (vars : List Name) where
  constructor MkEState
  {outer : List Name}
  -- The function/constructor name we're currently working on (resolved id)
  defining : Int
  -- The outer environment in which we're running the elaborator. Things here should
  -- be considered parametric as far as case expression elaboration goes, and are
  -- the only things that unbound implicits can depend on
  outerEnv : Env Term outer
  subEnv : SubVars outer vars
  boundNames : List (Name, ImplBinding vars)
                  -- implicit pattern/type variable bindings and the
                  -- term/type they elaborated to
  toBind : List (Name, ImplBinding vars)
                  -- implicit pattern/type variables which haven't been
                  -- bound yet. Record how they're bound (auto-implicit bound
                  -- pattern vars need to be dealt with in with-application on
                  -- the RHS)
  bindIfUnsolved : List (Name, RigCount,
                          (vars' ** (Env Term vars', PiInfo (Term vars'),
                                     Term vars', Term vars', SubVars outer vars')))
                  -- names to add as unbound implicits if they are still holes
                  -- when unbound implicits are added
  lhsPatVars : List Name
                  -- names which we've bound in elab mode InLHS (i.e. not
                  -- in a dot pattern). We keep track of this because every
                  -- occurrence other than the first needs to be dotted
  allPatVars : List Name
                  -- Holes standing for pattern variables, which we'll delete
                  -- once we're done elaborating
  polyMetavars : List (FC, Env Term vars, Term vars, Term vars)
                  -- Metavars which need to be a polymorphic type at the end
                  -- of elaboration. If they aren't, it means we're trying to
                  -- pattern match on a type that we don't have available.
  delayDepth : Nat -- if it gets too deep, it gets slow, so fail quicker
  linearUsed : List (Var vars)
  saveHoles : NameMap () -- things we'll need to save to TTC, even if solved

  unambiguousNames : UserNameMap (Name, Int, GlobalDef)
                  -- Mapping from userNameRoot to fully resolved names.
                  -- For names in this mapping, we don't run disambiguation.
                  -- Used in with-expressions.

export
data EST : Type where

export
initEStateSub : {outer : _} ->
                Int -> Env Term outer -> SubVars outer vars -> EState vars
initEStateSub n env sub = MkEState
    { defining = n
    , outerEnv = env
    , subEnv = sub
    , boundNames = []
    , toBind = []
    , bindIfUnsolved = []
    , lhsPatVars = []
    , allPatVars = []
    , polyMetavars = []
    , delayDepth = Z
    , linearUsed = []
    , saveHoles = empty
    , unambiguousNames = empty
    }

export
initEState : {vars : _} ->
             Int -> Env Term vars -> EState vars
initEState n env = initEStateSub n env SubRefl

export
saveHole : {auto e : Ref EST (EState vars)} ->
           Name -> Core ()
saveHole n
    = do est <- get EST
         put EST (record { saveHoles $= insert n () } est)

weakenedEState : {n, vars : _} ->
                 {auto e : Ref EST (EState vars)} ->
                 Core (Ref EST (EState (n :: vars)))
weakenedEState {e}
    = do est <- get EST
         eref <- newRef EST $
                   record { subEnv $= DropCons
                          , boundNames $= map wknTms
                          , toBind $= map wknTms
                          , linearUsed $= map weaken
                          , polyMetavars = [] -- no binders on LHS
                          } est
         pure eref
  where
    wknTms : (Name, ImplBinding vs) ->
             (Name, ImplBinding (n :: vs))
    wknTms (f, NameBinding c p x y)
        = (f, NameBinding c (map weaken p) (weaken x) (weaken y))
    wknTms (f, AsBinding c p x y z)
        = (f, AsBinding c (map weaken p) (weaken x) (weaken y) (weaken z))

strengthenedEState : {n, vars : _} ->
                     Ref Ctxt Defs ->
                     Ref EST (EState (n :: vars)) ->
                     FC -> Env Term (n :: vars) ->
                     Core (EState vars)
strengthenedEState {n} {vars} c e fc env
    = do est <- get EST
         defs <- get Ctxt
         svs <- dropSub (subEnv est)
         bns <- traverse (strTms defs) (boundNames est)
         todo <- traverse (strTms defs) (toBind est)
         pure $ record { subEnv = svs
                       , boundNames = bns
                       , toBind = todo
                       , linearUsed $= mapMaybe dropTop
                       , polyMetavars = [] -- no binders on LHS
                       } est

  where
    dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
    dropSub (DropCons sub) = pure sub
    dropSub _ = throw (InternalError "Badly formed weakened environment")

    -- Remove any instance of the top level local variable from an
    -- application. Fail if it turns out to be necessary.
    -- NOTE: While this isn't strictly correct given the type of the hole
    -- which stands for the unbound implicits, it's harmless because we
    -- never actualy *use* that hole - this process is only to ensure that the
    -- unbound implicit doesn't depend on any variables it doesn't have
    -- in scope.
    removeArgVars : List (Term (n :: vs)) -> Maybe (List (Term vs))
    removeArgVars [] = pure []
    removeArgVars (Local fc r (S k) p :: args)
        = do args' <- removeArgVars args
             pure (Local fc r _ (dropLater p) :: args')
    removeArgVars (Local fc r Z p :: args)
        = removeArgVars args
    removeArgVars (a :: args)
        = do a' <- shrinkTerm a (DropCons SubRefl)
             args' <- removeArgVars args
             pure (a' :: args')

    removeArg : Term (n :: vs) -> Maybe (Term vs)
    removeArg tm
        = case getFnArgs tm of
               (f, args) =>
                   do args' <- removeArgVars args
                      f' <- shrinkTerm f (DropCons SubRefl)
                      pure (apply (getLoc f) f' args')

    strTms : Defs -> (Name, ImplBinding (n :: vars)) ->
             Core (Name, ImplBinding vars)
    strTms defs (f, NameBinding c p x y)
        = do xnf <- normaliseHoles defs env x
             ynf <- normaliseHoles defs env y
             case (shrinkPi p (DropCons SubRefl),
                   removeArg xnf,
                   shrinkTerm ynf (DropCons SubRefl)) of
               (Just p', Just x', Just y') =>
                    pure (f, NameBinding c p' x' y')
               _ => throw (BadUnboundImplicit fc env f y)
    strTms defs (f, AsBinding c p x y z)
        = do xnf <- normaliseHoles defs env x
             ynf <- normaliseHoles defs env y
             znf <- normaliseHoles defs env z
             case (shrinkPi p (DropCons SubRefl),
                   shrinkTerm xnf (DropCons SubRefl),
                   shrinkTerm ynf (DropCons SubRefl),
                   shrinkTerm znf (DropCons SubRefl)) of
               (Just p', Just x', Just y', Just z') =>
                    pure (f, AsBinding c p' x' y' z')
               _ => throw (BadUnboundImplicit fc env f y)

    dropTop : (Var (n :: vs)) -> Maybe (Var vs)
    dropTop (MkVar First) = Nothing
    dropTop (MkVar (Later p)) = Just (MkVar p)

export
inScope : {n, vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto e : Ref EST (EState vars)} ->
          FC -> Env Term (n :: vars) ->
          (Ref EST (EState (n :: vars)) -> Core a) ->
          Core a
inScope {c} {e} fc env elab
    = do e' <- weakenedEState
         res <- elab e'
         st' <- strengthenedEState c e' fc env
         put {ref=e} EST st'
         pure res

export
mustBePoly : {auto e : Ref EST (EState vars)} ->
             FC -> Env Term vars ->
             Term vars -> Term vars -> Core ()
mustBePoly fc env tm ty
    = do est <- get EST
         put EST (record { polyMetavars $= ((fc, env, tm, ty) :: ) } est)

-- Return whether we already know the return type of the given function
-- type. If we know this, we can possibly infer some argument types before
-- elaborating them, which might help us disambiguate things more easily.
export
concrete : Defs -> Env Term vars -> NF vars -> Core Bool
concrete defs env (NBind fc _ (Pi _ _ _ _) sc)
    = do sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
         concrete defs env sc'
concrete defs env (NDCon _ _ _ _ _) = pure True
concrete defs env (NTCon _ _ _ _ _) = pure True
concrete defs env (NPrimVal _ _) = pure True
concrete defs env (NType _) = pure True
concrete defs env _ = pure False

export
updateEnv : {new : _} ->
            Env Term new -> SubVars new vars ->
            List (Name, RigCount,
                   (vars' ** (Env Term vars', PiInfo (Term vars'),
                              Term vars', Term vars', SubVars new vars'))) ->
            EState vars -> EState vars
updateEnv env sub bif st
    = record { outerEnv = env
             , subEnv = sub
             , bindIfUnsolved = bif
             } st

export
addBindIfUnsolved : {vars : _} ->
                    Name -> RigCount -> PiInfo (Term vars) ->
                    Env Term vars -> Term vars -> Term vars ->
                    EState vars -> EState vars
addBindIfUnsolved hn r p env tm ty st
    = record { bindIfUnsolved $=
                ((hn, r, (_ ** (env, p, tm, ty, subEnv st))) ::)} st

clearBindIfUnsolved : EState vars -> EState vars
clearBindIfUnsolved = record { bindIfUnsolved = [] }

-- Clear the 'toBind' list, except for the names given
export
clearToBind : {auto e : Ref EST (EState vars)} ->
              (excepts : List Name) -> Core ()
clearToBind excepts
    = do est <- get EST
         put EST (record { toBind $= filter (\x => fst x `elem` excepts) }
                         (clearBindIfUnsolved est))

export
noteLHSPatVar : {auto e : Ref EST (EState vars)} ->
                ElabMode -> Name -> Core ()
noteLHSPatVar (InLHS _) n
    = do est <- get EST
         put EST (record { lhsPatVars $= (n ::) } est)
noteLHSPatVar _ _ = pure ()

export
notePatVar : {auto e : Ref EST (EState vars)} ->
             Name -> Core ()
notePatVar n
    = do est <- get EST
         put EST (record { allPatVars $= (n ::) } est)

export
metaVar : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          FC -> RigCount ->
          Env Term vars -> Name -> Term vars -> Core (Term vars)
metaVar fc rig env n ty
    = do (_, tm) <- newMeta fc rig env n ty (Hole (length env) (holeInit False)) True
         pure tm

export
implBindVar : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              Env Term vars -> Name -> Term vars -> Core (Term vars)
implBindVar fc rig env n ty
    = do (_, tm) <- newMeta fc rig env n ty (Hole (length env) (holeInit True)) True
         pure tm

export
metaVarI : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           FC -> RigCount ->
           Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
metaVarI fc rig env n ty
    = do defs <- get Ctxt
         tynf <- nf defs env ty
         let hinf = case tynf of
                         NApp _ (NMeta _ _ _) _ =>
                              record { precisetype = True } (holeInit False)
                         _ => holeInit False
         newMeta fc rig env n ty (Hole (length env) hinf) True

export
argVar : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         FC -> RigCount ->
         Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
argVar fc rig env n ty
    = newMetaLets fc rig env n ty (Hole (length env) (holeInit False)) False True

export
searchVar : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            FC -> RigCount -> Nat -> Name ->
            Env Term vars -> NestedNames vars -> Name -> Term vars -> Core (Term vars)
searchVar fc rig depth def env nest n ty
    = do defs <- get Ctxt
         (vars' ** (bind, env')) <- envHints (keys (localHints defs)) env
         -- Initial the search with an environment which binds the applied
         -- local hints
         (_, tm) <- newSearch fc rig depth def env' n
                              (weakenNs (mkSizeOf vars') ty)
         pure (bind tm)
  where
    useVars : {vars : _} ->
              List (Term vars) -> Term vars -> Term vars
    useVars [] sc = sc
    useVars (a :: as) (Bind bfc n (Pi fc c _ ty) sc)
         = Bind bfc n (Let fc c a ty) (useVars (map weaken as) sc)
    useVars as (Bind bfc n (Let fc c v ty) sc)
         = Bind bfc n (Let fc c v ty) (useVars (map weaken as) sc)
    useVars _ sc = sc -- Can't happen?

    find : Name -> List (Name, (Maybe Name, b)) -> Maybe (Maybe Name, b)
    find x [] = Nothing
    find x ((n, t) :: xs)
       = if x == n
            then Just t
            else case t of
                      (Nothing, _) => find x xs
                      (Just n', _) => if x == n'
                                         then Just t
                                         else find x xs

    envHints : List Name -> Env Term vars ->
               Core (vars' ** (Term (vars' ++ vars) -> Term vars, Env Term (vars' ++ vars)))
    envHints [] env = pure ([] ** (id, env))
    envHints (n :: ns) env
        = do (vs ** (f, env')) <- envHints ns env
             let Just (nestn, argns, tmf) = find !(toFullNames n) (names nest)
                 | Nothing => pure (vs ** (f, env'))
             let n' = maybe n id nestn
             defs <- get Ctxt
             Just ndef <- lookupCtxtExact n' (gamma defs)
                 | Nothing => pure (vs ** (f, env'))
             let nt = fromMaybe Func (defNameType $ definition ndef)
             let app = tmf fc nt
             let tyenv = useVars (getArgs app) (embed (type ndef))
             let binder = Let fc top (weakenNs (mkSizeOf vs) app)
                                     (weakenNs (mkSizeOf vs) tyenv)
             varn <- toFullNames n'
             pure ((varn :: vs) **
                    (\t => f (Bind fc varn binder t),
                       binder :: env'))

-- Elaboration info (passed to recursive calls)
public export
record ElabInfo where
  constructor MkElabInfo
  elabMode : ElabMode
  implicitMode : BindMode
  topLevel : Bool
  bindingVars : Bool
  preciseInf : Bool -- are types inferred precisely (True) or do we generalise
                    -- pi bindings to RigW (False, default)
  ambigTries : List Name

export
initElabInfo : ElabMode -> ElabInfo
initElabInfo m = MkElabInfo m NONE False True False []

export
tryError : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           Core a -> Core (Either Error a)
tryError elab
    = do ust <- get UST
         est <- get EST
         md <- get MD
         defs <- branch
         catch (do res <- elab
                   commit
                   pure (Right res))
               (\err => do put UST ust
                           put EST est
                           put MD md
                           defs' <- get Ctxt
                           put Ctxt (record { timings = timings defs' } defs)
                           pure (Left err))

export
try : {vars : _} ->
      {auto c : Ref Ctxt Defs} ->
      {auto m : Ref MD Metadata} ->
      {auto u : Ref UST UState} ->
      {auto e : Ref EST (EState vars)} ->
      Core a -> Core a -> Core a
try elab1 elab2
    = do Right ok <- tryError elab1
               | Left err => elab2
         pure ok

export
handle : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto m : Ref MD Metadata} ->
         {auto u : Ref UST UState} ->
         {auto e : Ref EST (EState vars)} ->
         Core a -> (Error -> Core a) -> Core a
handle elab1 elab2
    = do Right ok <- tryError elab1
               | Left err => elab2 err
         pure ok

successful : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             Bool -> -- constraints allowed
             List (Maybe Name, Core a) ->
             Core (List (Either (Maybe Name, Error)
                                (Nat, a, Defs, UState, EState vars, Metadata)))
successful allowCons [] = pure []
successful allowCons ((tm, elab) :: elabs)
    = do ust <- get UST
         let ncons = if allowCons
                        then 0
                        else length (toList (guesses ust))
         est <- get EST
         md <- get MD
         defs <- branch
         catch (do -- Run the elaborator
                   logC "elab" 5 $
                            do tm' <- maybe (pure (UN $ Basic "__"))
                                             toFullNames tm
                               pure ("Running " ++ show tm')
                   res <- elab
                   -- Record post-elaborator state
                   ust' <- get UST
                   let ncons' = if allowCons
                                   then 0
                                   else length (toList (guesses ust'))

                   est' <- get EST
                   md' <- get MD
                   defs' <- get Ctxt

                   -- Reset to previous state and try the rest
                   put UST ust
                   put EST est
                   put MD md
                   put Ctxt defs
                   logC "elab" 5 $
                            do tm' <- maybe (pure (UN $ Basic "__"))
                                            toFullNames tm
                               pure ("Success " ++ show tm' ++
                                     " (" ++ show ncons' ++ " - "
                                          ++ show ncons ++ ")")
                   elabs' <- successful allowCons elabs
                   -- Record success, and the state we ended at
                   pure (Right (minus ncons' ncons,
                                res, defs', ust', est', md') :: elabs'))
               (\err => do put UST ust
                           put EST est
                           put MD md
                           put Ctxt defs
                           when (abandon err) $ throw err
                           elabs' <- successful allowCons elabs
                           pure (Left (tm, err) :: elabs'))
  where
    -- Some errors, it's not worth trying all the possibilities because
    -- something serious has gone wrong, so just give up immediately.
    abandon : Error -> Bool
    abandon (UndefinedName _ _) = True
    abandon (InType _ _ err) = abandon err
    abandon (InCon _ _ err) = abandon err
    abandon (InLHS _ _ err) = abandon err
    abandon (InRHS _ _ err) = abandon err
    abandon (AllFailed errs) = any (abandon . snd) errs
    abandon _ = False

export
exactlyOne' : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto e : Ref EST (EState vars)} ->
              Bool -> FC -> Env Term vars ->
              List (Maybe Name, Core (Term vars, Glued vars)) ->
              Core (Term vars, Glued vars)
exactlyOne' allowCons fc env [(tm, elab)] = elab
exactlyOne' {vars} allowCons fc env all
    = do elabs <- successful allowCons all
         case getRight elabs of
              Right (res, defs, ust, est, md) =>
                    do put UST ust
                       put EST est
                       put MD  md
                       put Ctxt defs
                       commit
                       pure res
              Left rs => throw (altError (lefts elabs) rs)
  where
    getRight : List (Either err (Nat, res)) -> Either (List res) res
    getRight es
        = case rights es of
               [(_, res)] => Right res
               rs => case filter (\x => fst x == Z) rs of
                          [(_, res)] => Right res
                          _ => Left (map snd rs)

    getRes : ((Term vars, Glued vars), st) -> Term vars
    getRes ((tm, _), thisst) = tm

    getDepthError : Error -> Maybe Error
    getDepthError e@(AmbiguityTooDeep _ _ _) = Just e
    getDepthError _ = Nothing

    depthError : List (Maybe Name, Error) -> Maybe Error
    depthError [] = Nothing
    depthError ((_, e) :: es)
        = maybe (depthError es) Just (getDepthError e)

    -- If they've all failed, collect all the errors
    -- If more than one succeeded, report the ambiguity
    altError : List (Maybe Name, Error) ->
               List ((Term vars, Glued vars), st) ->
               Error
    altError ls []
        = case depthError ls of
               Nothing => AllFailed ls
               Just err => err
    altError ls rs = AmbiguousElab fc env (map getRes rs)

export
exactlyOne : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             FC -> Env Term vars ->
             List (Maybe Name, Core (Term vars, Glued vars)) ->
             Core (Term vars, Glued vars)
exactlyOne = exactlyOne' True

export
anyOne : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto m : Ref MD Metadata} ->
         {auto u : Ref UST UState} ->
         {auto e : Ref EST (EState vars)} ->
         FC -> List (Maybe Name, Core (Term vars, Glued vars)) ->
         Core (Term vars, Glued vars)
anyOne fc [] = throw (GenericMsg fc "No elaborators provided")
anyOne fc [(tm, elab)] = elab
anyOne fc ((tm, elab) :: es) = try elab (anyOne fc es)

-- Implemented in TTImp.Elab.Term; delaring just the type allows us to split
-- the elaborator over multiple files more easily
export
check : {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 -> RawImp ->
        Maybe (Glued vars) ->
        Core (Term vars, Glued vars)

-- As above, but doesn't add any implicit lambdas, forces, delays, etc
export
checkImp : {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 -> RawImp -> Maybe (Glued vars) ->
           Core (Term vars, Glued vars)

-- Implemented in TTImp.ProcessDecls
export
processDecl : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              List ElabOpt -> NestedNames vars ->
              Env Term vars -> ImpDecl -> Core ()

-- Check whether two terms are convertible. May solve metavariables (in Ctxt)
-- in doing so.
-- Returns a list of constraints which need to be solved for the conversion
-- to work; if this is empty, the terms are convertible.
convertWithLazy
        : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto e : Ref EST (EState vars)} ->
          (withLazy : Bool) ->
          FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
          Core UnifyResult
convertWithLazy withLazy fc elabinfo env x y
    = let umode : UnifyInfo
                = case elabMode elabinfo of
                       InLHS _ => inLHS
                       _ => inTerm in
          catch
            (do let lazy = !isLazyActive && withLazy
                logGlueNF "elab.unify" 5 ("Unifying " ++ show withLazy ++ " "
                             ++ show (elabMode elabinfo)) env x
                logGlueNF "elab.unify" 5 "....with" env y
                vs <- if isFromTerm x && isFromTerm y
                         then do xtm <- getTerm x
                                 ytm <- getTerm y
                                 if lazy
                                    then unifyWithLazy umode fc env xtm ytm
                                    else unify umode fc env xtm ytm
                         else do xnf <- getNF x
                                 ynf <- getNF y
                                 if lazy
                                    then unifyWithLazy umode fc env xnf ynf
                                    else unify umode fc env xnf ynf
                when (holesSolved vs) $
                    solveConstraints umode Normal
                pure vs)
            (\err =>
               do defs <- get Ctxt
                  xtm <- getTerm x
                  ytm <- getTerm y
                  -- See if we can improve the error message by
                  -- resolving any more constraints
                  catch (solveConstraints umode Normal)
                        (\err => pure ())
                  -- We need to normalise the known holes before
                  -- throwing because they may no longer be known
                  -- by the time we look at the error
                  defs <- get Ctxt
                  throw (WhenUnifying fc (gamma defs) env xtm ytm err))

export
convert : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto e : Ref EST (EState vars)} ->
          FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
          Core UnifyResult
convert = convertWithLazy False

-- Check whether the type we got for the given type matches the expected
-- type.
-- Returns the term and its type.
-- This may generate new constraints; if so, the term returned is a constant
-- guarded by the constraints which need to be solved.
export
checkExp : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           RigCount -> ElabInfo -> Env Term vars -> FC ->
           (term : Term vars) ->
           (got : Glued vars) -> (expected : Maybe (Glued vars)) ->
           Core (Term vars, Glued vars)
checkExp rig elabinfo env fc tm got (Just exp)
    = do vs <- convertWithLazy True fc elabinfo env got exp
         case (constraints vs) of
              [] => case addLazy vs of
                         NoLazy => do logTerm "elab" 5 "Solved" tm
                                      pure (tm, got)
                         AddForce r => do logTerm "elab" 5 "Force" tm
                                          logGlue "elab" 5 "Got" env got
                                          logGlue "elab" 5 "Exp" env exp
                                          pure (TForce fc r tm, exp)
                         AddDelay r => do ty <- getTerm got
                                          logTerm "elab" 5 "Delay" tm
                                          pure (TDelay fc r ty tm, exp)
              cs => do logTerm "elab" 5 "Not solved" tm
                       defs <- get Ctxt
                       empty <- clearDefs defs
                       cty <- getTerm exp
                       ctm <- newConstant fc rig env tm cty cs
                       dumpConstraints "elab" 5 False
                       case addLazy vs of
                            NoLazy => pure (ctm, got)
                            AddForce r => pure (TForce fc r tm, exp)
                            AddDelay r => do ty <- getTerm got
                                             pure (TDelay fc r ty tm, exp)
checkExp rig elabinfo env fc tm got Nothing = pure (tm, got)


text:
-- ------------------------------------------------------------ [ ArgParse.idr ]
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Commons.Options.ArgParse

import Commons.Options.ArgParse.Lexer
import Commons.Options.ArgParse.Parser

import public Commons.Options.ArgParse.Model

import Commons.Options.ArgParse.Parser
import public Commons.Options.ArgParse.Error

%access export
%default total
-- ----------------------------------------------------------------- [ Records ]

private
convOpts : (Arg -> a -> Maybe a)
        -> a
        -> List Arg
        -> Either ArgParseError a
convOpts  _   o Nil       = pure o
convOpts conv o (x :: xs) = case conv x o of
    Nothing => Left (InvalidOption x)
    Just o' => do
      os <- convOpts conv o' xs
      pure os

||| Parse arguments using a record.
|||
||| @orig The starting value of the record representing the options.
||| @conv A user supplied conversion function used to update the record.
||| @args The *unmodified* result of calling `System.getArgs` or `Effects.System.geArgs`.
parseArgs : (orig : a)
         -> (conv : Arg -> a -> Maybe a)
         -> (args : List String)
         -> Either ArgParseError a
parseArgs o _    Nil     = pure o
parseArgs o _    [a]     = pure o
parseArgs o func (a::as) = do
    case parseArgsStr (unwords as) of
      Left err  => Left (MalformedOption err)
      Right res => do
        r <- convOpts func o res
        pure r

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
-- Things like  ( , )  ( ** )  ()   are special in that they denote more than
-- one thing at once. () can mean Unit or MkUnit, (,) can mean Pair or MkPair
-- Idiom brackets need to be able to work despite that, which is tested here

fez : IO Int
fez = pure 1

fez1 : IO (Int, ())
fez1 = [| MkPair fez (pure ()) |]

fez2 : IO (Int, Maybe Int)
fez2 = [| ( fez , (pure Nothing) ) |]


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor
   Ctrl-Alt-W: Add With View -}
module Main

data TakeN : List a -> Type where
  Fewer : TakeN xs
  Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) = case takeN k xs of
  Fewer => Fewer
  Exact ys => Exact (x :: ys)

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

halves : List a -> (List a, List a)
halves xs with (takeN (length xs `div` 2) xs)
  halves xs | Fewer = (xs, [])
  halves (n_xs ++ rest) | (Exact n_xs) = (n_xs, rest)

main : IO ()
main = do
  printLn $ groupByN 3 [1,2,3,4,5,6,7,8,9,10,11]
  printLn $ halves [1..10]
  printLn $ halves [1]

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module Ch05.Exercise_5_2_1

import Ch05.LambdaCalculus

%default total

or : Term
or = Abs 0 (Abs 1 (App (App (Var 0) tru) (Var 1)))

not : Term
not = Abs 0 (Abs 1 (Abs 2 (App (App (Var 0) (Var 2)) (Var 1))))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module TicTactoe

import Data.Fin as F
import Data.String as S
import Data.Vect as V

import ConsoleIO

%default total

-- Convenient alias for sized Matrix type
--
Matrix : Nat -> Nat -> Type -> Type
Matrix r c a = Vect r (Vect c a)

-- Filling in some of the game types
--
data Player = X | O

Eq Player where
  X == X = True
  O == O = True
  _ == _ = False

data GameResult = Win Player | Draw | InPlay

Board : Type
Board = Matrix 3 3 (Maybe Player)

mkEmptyBoard : Board
mkEmptyBoard = replicate 3 $ replicate 3 Nothing

idxMat : Fin n -> Fin m -> Matrix n m a -> a
idxMat r c m = index c (index r m)

gameRes : Board -> GameResult
gameRes b =
  if winFor X
  then Win X
  else if winFor O
       then Win O
       else if (all isJust (concat b))
            then Draw
            else InPlay

  where winFor : Player -> Bool
        winFor p =
          let bools = map (map (== (Just p))) b
          in  (any (all id) bools)
              || (any (all id) (transpose bools))
              || (all id (the (Vect _ Bool) [idxMat 0 0 bools, idxMat 1 1 bools, idxMat 2 2 bools]))
              || (all id (the (Vect _ Bool) [idxMat 2 0 bools, idxMat 1 1 bools, idxMat 0 2 bools]))

tryPlayPiece  : Fin 3 -> Fin 3 -> Player -> Board -> Maybe Board
tryPlayPiece r c p b =
  case idxMat r c b of
    Just _  => Nothing
    Nothing =>
      let newBoard = playPiece r c p b
      in  Just newBoard
  where playPiece : Fin 3 -> Fin 3 -> Player -> Board -> Board
        playPiece row col pc board =
          let theRow = index row board
          in  replaceAt row (replaceAt col (Just pc) theRow) board

computerPlay : Board -> Maybe Board
computerPlay b =
      tryPlayPiece 1 1 O b
  <+> tryPlayPiece 0 0 O b
  <+> tryPlayPiece 2 2 O b
  <+> tryPlayPiece 0 2 O b
  <+> tryPlayPiece 2 0 O b
  <+> tryPlayPiece 0 1 O b
  <+> tryPlayPiece 1 0 O b
  <+> tryPlayPiece 1 2 O b
  <+> tryPlayPiece 2 1 O b

data Input
  = Index (Fin 3) (Fin 3)
  | Done
  | Oops

parseFin : String -> Maybe (Fin 3)
parseFin s = parseInteger s >>= \i => integerToFin i 3

readInput : ConsoleCmnd Input
readInput =
  do PutStr "\nEnter row and column indices separated by a space, q to quit: "
     rowS <- GetLine
     case span (/= ' ') rowS of
       ("q","")  => Pure Done
       (row,col) =>
         case (parseFin row, parseFin col) of
           (Just r, Just c) => Pure (Index r c)
           _                => Pure Oops

rowToString : Vect n (Maybe Player) -> String
rowToString = (++ "\n") . concat . intersperse "|" . map toStr
  where toStr : Maybe Player -> String
        toStr Nothing  = "   "
        toStr (Just X) = " X "
        toStr (Just O) = " O "

printBoard : Board -> ConsoleCmnd ()
printBoard b =
  traverse_ PutStr (intersperse "-----------\n" (map rowToString b))

data Result = XWin | XLose | NoWinner | Quitter

tictactoe : Board -> ConsoleIO Result
tictactoe b =
  do PutStr "The current state of affairs:\n\n"
     printBoard b
     input <- readInput
     case input of
       Index r c =>
         case (tryPlayPiece r c X b) of
           Nothing => do PutStr "You can't write on top of another player's piece!\n"
                         tictactoe b
           Just b  => do printBoard b
                         case gameRes b of
                           Win X  => Quit XWin
                           Win O  => Quit XLose
                           Draw   => Quit NoWinner
                           InPlay => computerPlay' b
       Done      => Quit Quitter
       Oops      => do PutStr "You mistyped.  Let's try again\n"
                       tictactoe b
   where computerPlay' : Board -> ConsoleIO Result
         computerPlay' b =
           case computerPlay b of
             Nothing => do PutStr "That's weird!\n"
                           Quit Quitter
             Just b' => case gameRes b' of
                          Win X  => Quit XWin
                          Win O  => Quit XLose
                          Draw   => Quit NoWinner
                          InPlay => tictactoe b'

main : IO ()
main = do
  putStrLn "How about a nice game of tic tac toe?\n\n"
  result <- runConsoleIO (tank 1000) (tictactoe mkEmptyBoard)
  putStrLn "\n"
  case result of
    Nothing       => putStrLn "Goodbye."
    Just XWin     => putStrLn "Congratulations, you win!"
    Just XLose    => putStrLn "Sorry, you lose!"
    Just NoWinner => putStrLn "Game is a draw!"
    Just Quitter  => putStrLn "Why you quit?"
  putStrLn "\n"

max_stars_repo_name: braje/totality-talk

max_issues_repo_name: braje/totality-talk

max_forks_repo_name: braje/totality-talk


text:
module Equivalence

-- Proof that small-step and big-step semantics for
-- the simply-typed lambda calculus are equivalent.

import BigStep
import Step
import Subst
import Term

%default total
%access export

--------------------------
-- Begin: STEP => BIG-STEP

stepToBigStep : Step e1 e2 -> BigStep e2 e3 ->
                BigStep e1 e3
-- case split in the following order: (Step e1 e2), (BigStep e2 e3)
stepToBigStep (StRec x) (BStValue _) impossible
--
stepToBigStep (StRec x) (BStRecZero z w) = let ih = stepToBigStep x z
                                           in BStRecZero ih w
--
stepToBigStep (StRec x) (BStRecSucc y z) = let ih = stepToBigStep x y
                                           in BStRecSucc ih z
--
stepToBigStep StRecZero x = BStRecZero (BStValue VZero) x
--
stepToBigStep (StRecSucc x) y = BStRecSucc (BStValue x) y

stepToBigStep (StApp1 x) (BStValue _) impossible
--
stepToBigStep (StApp1 x) (BStApp w s1 t1) = let ih = stepToBigStep x w
                                            in BStApp ih s1 t1
--
stepToBigStep (StApp2 x z) (BStValue v) impossible
--
stepToBigStep (StApp2 x z) (BStApp s1 t1 u) = let ih = stepToBigStep z t1
                                              in BStApp s1 ih u
--
stepToBigStep (StBeta x) y = BStApp (BStValue VAbs) (BStValue x) y
--
stepToBigStep (StSucc x) (BStValue v) = case v of
  VAbs     impossible
  VZero    impossible
  VSucc v' => BStSucc $ stepToBigStep x (BStValue v')
--
stepToBigStep (StSucc x) (BStSucc y) = BStSucc $ stepToBigStep x y
--
stepToBigStep (StPred x) (BStValue _) impossible
--
stepToBigStep (StPred x) (BStPredZero z) = BStPredZero $ stepToBigStep x z
--
stepToBigStep (StPred x) (BStPredSucc y) = let ih = stepToBigStep x y
                                           in BStPredSucc ih
--
stepToBigStep StPredZero (BStValue _) = BStPredZero (BStValue VZero)
--
stepToBigStep (StPredSucc x) y = BStPredSucc (BStSucc y)
--
stepToBigStep (StIfz x) (BStValue _) impossible
--
stepToBigStep (StIfz x) (BStIfzZero z w) = let ih = stepToBigStep x z
                                           in BStIfzZero ih w
--
stepToBigStep (StIfz x) (BStIfzSucc w s) = let ih = stepToBigStep x w
                                           in BStIfzSucc ih s
--
stepToBigStep StIfzZero y = BStIfzZero (BStValue VZero) y
--
stepToBigStep (StIfzSucc x) y = BStIfzSucc (BStValue (VSucc x)) y

-- End: STEP => BIG-STEP
------------------------

-------------------------------
-- Begin: TRANSSTEP => BIG-STEP

transStepToBigStep : (TransStep e1 e2) -> (v : Value e2) ->
                     BigStep e1 e2
transStepToBigStep (TStRefl _)    v = BStValue v
transStepToBigStep (TStTrans x y) v = let ih = transStepToBigStep y v
                                      in stepToBigStep x ih

-- End: TRANSSTEP => BIG-STEP
-----------------------------

-------------------------------
-- Begin: BIG-STEP => TRANSSTEP

-- Congruence lemma for '(TApp _ e)':
congApp1 : TransStep e1 e2 -> TransStep (TApp e1 e) (TApp e2 e)
congApp1 (TStRefl e1)   = TStRefl (TApp e1 _)
congApp1 (TStTrans x y) = TStTrans (StApp1 x) (congApp1 y)

-- Congruence lemma for '(TApp e _)':
congApp2 : {v : Value e} ->
           TransStep e1 e2 -> TransStep (TApp e e1) (TApp e e2)
congApp2         (TStRefl e1)   = TStRefl (TApp _ e1)
congApp2 {v = v} (TStTrans x y) = TStTrans (StApp2 v x) (congApp2 {v = v} y)

-- Congruence lemma for '(Succ _)':
congSucc : TransStep e1 e2 -> TransStep (TSucc e1) (TSucc e2)
congSucc (TStRefl e1)   = TStRefl (TSucc e1)
congSucc (TStTrans x y) = TStTrans (StSucc x) (congSucc y)

-- Congruence lemma for '(Pred _)':
congPred : TransStep e1 e2 -> TransStep (TPred e1) (TPred e2)
congPred (TStRefl e1)   = TStRefl (TPred e1)
congPred (TStTrans x y) = TStTrans (StPred x) (congPred y)

-- Congruence lemma for '(Ifz _ ez es)':
congIfz : TransStep e1 e2 -> TransStep (TIfz e1 ez es) (TIfz e2 ez es)
congIfz (TStRefl e1)   = TStRefl (TIfz e1 _ _)
congIfz (TStTrans x y) = TStTrans (StIfz x) (congIfz y)

-- Congruence lemma for '(TRec _ e0 e1)':
congRec : TransStep e e' -> TransStep (TRec e e0 e1) (TRec e' e0 e1)
congRec (TStRefl e)    = TStRefl (TRec e _ _)
congRec (TStTrans x y) = TStTrans (StRec x) (congRec y)

bigStepToTransStep : BigStep e1 e2 -> (TransStep e1 e2, Value e2)
--
bigStepToTransStep (BStRecZero y z) =
  let (tst1, v1) = bigStepToTransStep y
      (tst2, v2) = bigStepToTransStep z
      tst = (congRec tst1) .+. StRecZero .++. tst2
  in (tst, v2)
--
bigStepToTransStep (BStRecSucc x y) =
  let (tst1, v1) = bigStepToTransStep x
      (tst2, v2) = bigStepToTransStep y
      tst = (congRec tst1) .+. (StRecSucc v1) .++. tst2
  in (tst, v2)
--
bigStepToTransStep (BStValue v) = (TStRefl _, v)
--
bigStepToTransStep (BStApp z w t1) =
  let (tst1, v1) = bigStepToTransStep z
      (tst2, v2) = bigStepToTransStep w
      (tst3, v3) = bigStepToTransStep t1
      tst = (congApp1 tst1) .++. (congApp2 {v = VAbs} tst2) .+. (StBeta v2) .++. tst3
  in (tst, v3)
--
bigStepToTransStep (BStSucc x) =
  let (tst1, v1) = bigStepToTransStep x
  in (congSucc tst1, VSucc v1)
--
bigStepToTransStep (BStPredZero y) =
  let (tst1, v1) = bigStepToTransStep y
      tst = congPred tst1 .+. StPredZero
  in (tst, VZero)
--
bigStepToTransStep (BStPredSucc x) =
  let (tst1, VSucc v1) = bigStepToTransStep x
      tst = (congPred tst1) .+. (StPredSucc v1)
  in (tst, v1)

bigStepToTransStep (BStIfzZero z w) =
  let (tst1, v1) = bigStepToTransStep z
      (tst2, v2) = bigStepToTransStep w
      tst = (congIfz tst1) .+. StIfzZero .++. tst2
  in (tst, v2)

bigStepToTransStep (BStIfzSucc w s) =
  let (tst1, VSucc v1) = bigStepToTransStep w
      (tst2, v2) = bigStepToTransStep s
      tst = (congIfz tst1) .+. (StIfzSucc v1) .++. tst2
  in (tst, v2)

-- End: BIG-STEP => TRANSSTEP
-----------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Toolkit.Data.DList.Interleaving

import public Toolkit.Data.List.Interleaving

import Toolkit.Data.DList

%default total

public export
data Interleaving : (a : Type)
                 -> (type : a -> Type)
                 -> {ls, rs, os : List a}
                 -> (lefts  : DList a type ls)
                 -> (rights : DList a type rs)
                 -> (orig   : DList a type os)
                 -> (prf    : Interleaving ls rs os)
                           -> Type
  where
    Empty : Interleaving a type Nil Nil Nil Empty

    Left  : {a : Type}
         -> {type : a -> Type}
         -> {x : a}
         -> {xs, ys, zs : List a}
         -> {ls   : DList a type xs}
         -> {rs   : DList a type ys}
         -> {os   : DList a type zs}
         -> {prf  : Interleaving xs ys zs}
         -> (head : type x)
         -> (tail : Interleaving a type        ls  rs        os         prf)
                 -> Interleaving a type (head::ls) rs (head::os) (x <:: prf)

    Right : {a : Type}
         -> {type : a -> Type}
         -> {y : a}
         -> {xs, ys, zs : List a}
         -> {ls   : DList a type xs}
         -> {rs   : DList a type ys}
         -> {os   : DList a type zs}
         -> {prf  : Interleaving xs ys zs}
         -> (head : type y)
         -> (tail : Interleaving a type ls        rs         os         prf)
                 -> Interleaving a type ls (head::rs) (head::os) (y ::> prf)

(<::) : {a : Type}
     -> {type : a -> Type}
     -> {x    : a}
     -> {xs, ys, zs : List a}
     -> {ls   : DList a type xs}
     -> {rs   : DList a type ys}
     -> {os   : DList a type zs}
     -> {prf  : Interleaving xs ys zs}
     -> (head : type x)
     -> (tail : Interleaving a type        ls  rs        os         prf)
             -> Interleaving a type (head::ls) rs (head::os) (x <:: prf)
(<::) = Left

(::>) : {a : Type}
     -> {type : a -> Type}
     -> {xs, ys, zs : List a}
     -> {ls   : DList a type xs}
     -> {rs   : DList a type ys}
     -> {os   : DList a type zs}
     -> {prf  : Interleaving xs ys zs}
     -> {y    : a}
     -> (head : type y)
     -> (tail : Interleaving a type ls        rs         os         prf)
             -> Interleaving a type ls (head::rs) (head::os) (y ::> prf)
(::>) = Right

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module System.Directory

import public System.File
import System.FFI

%default total

public export
DirPtr : Type
DirPtr = AnyPtr

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_directory.h"

directoriesClass : String
directoriesClass = "io/github/mmhelloworld/idrisjvm/runtime/Directories"

%foreign "C:idris2_fileErrno, libidris2_support, idris_file.h"
         "node:support:fileErrno,support_system_file"
         jvm' runtimeClass "getErrorNumber" "java/lang/Object" "int"
prim__fileErrno : PrimIO Int

returnError : HasIO io => io (Either FileError a)
returnError
    = do err <- primIO prim__fileErrno
         pure $ Left $
           case err of
              0 => FileReadError
              1 => FileWriteError
              2 => FileNotFound
              3 => PermissionDenied
              4 => FileExists
              _ => GenericFileError (err-5)

ok : HasIO io => a -> io (Either FileError a)
ok x = pure (Right x)

%foreign support "idris2_currentDirectory"
         "node:lambda:()=>process.cwd()"
         jvm directoriesClass "getWorkingDirectory"
prim__currentDir : PrimIO (Ptr String)

%foreign support "idris2_changeDir"
         "node:support:changeDir,support_system_directory"
         jvm directoriesClass "changeDirectory"
prim__changeDir : String -> PrimIO Int

%foreign support "idris2_createDir"
         "node:support:createDir,support_system_directory"
         jvm directoriesClass "createDirectory"
prim__createDir : String -> PrimIO Int

%foreign support "idris2_openDir"
         jvm directoriesClass "openDirectory"
prim__openDir : String -> PrimIO DirPtr

%foreign support "idris2_closeDir"
         jvm directoriesClass "closeDirectory"
prim__closeDir : DirPtr -> PrimIO ()

%foreign support "idris2_removeDir"
         jvm directoriesClass "delete"
prim__removeDir : String -> PrimIO ()

%foreign support "idris2_nextDirEntry"
         jvm directoriesClass "getNextDirectoryEntry"
prim__dirEntry : DirPtr -> PrimIO (Ptr String)

export
data Directory : Type where
     MkDir : DirPtr -> Directory

export
createDir : HasIO io => String -> io (Either FileError ())
createDir dir
    = do res <- primIO (prim__createDir dir)
         if res == 0
            then ok ()
            else returnError

export
changeDir : HasIO io => String -> io Bool
changeDir dir
    = do ok <- primIO (prim__changeDir dir)
         pure (ok == 0)

export
currentDir : HasIO io => io (Maybe String)
currentDir
    = do res <- primIO prim__currentDir
         if prim__nullPtr res /= 0
            then pure Nothing
            else pure (Just (prim__getString res))

export
openDir : HasIO io => String -> io (Either FileError Directory)
openDir d
    = do res <- primIO (prim__openDir d)
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (MkDir res)

export
closeDir : HasIO io => Directory -> io ()
closeDir (MkDir d) = primIO (prim__closeDir d)

export
removeDir : HasIO io => String -> io ()
removeDir dirName = primIO (prim__removeDir dirName)

export
dirEntry : HasIO io => Directory -> io (Either FileError String)
dirEntry (MkDir d)
    = do res <- primIO (prim__dirEntry d)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
||| Definition and helper functions related to the LSP server implementation configuration.
|||
||| (C) The Idris Community, 2021
module Server.Configuration

import Language.LSP.Message.Initialize
import Language.LSP.Message.URI
import System.File

||| Label for the configuration reference.
public export
data LSPConf : Type where

||| Type for the LSP server configuration.
public export
record LSPConfiguration where
  constructor MkLSPConfiguration
  ||| File handle where to read LSP messages.
  inputHandle : File
  ||| File handle where to output LSP messages.
  outputHandle : File
  ||| File handle where to put log messages.
  logHandle : File
  ||| If the initialization protocol has succeded, it contains the client configuration.
  ||| @see https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/#initialize
  initialized : Maybe InitializeParams
  ||| True if the client has completed the shutdown protocol.
  ||| @see https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/#shutdown
  isShutdown : Bool
  ||| The currently loaded file, if any, and its version.
  openFile : Maybe (DocumentURI, Int)
  ||| Limit for multiple search results
  searchLimit : Nat

||| Server default configuration. Uses standard input and standard output for input/output.
export
defaultConfig : LSPConfiguration
defaultConfig = MkLSPConfiguration { inputHandle = stdin
                                   , outputHandle = stdout
                                   , logHandle = stderr
                                   , initialized = Nothing
                                   , isShutdown = False
                                   , openFile = Nothing
                                   , searchLimit = 5
                                   }


text:
module Control.Monad.ST

import Data.IORef

export
data STRef : Type -> Type -> Type where
     MkSTRef : IORef a -> STRef s a

export
data ST : Type -> Type -> Type where
     MkST : IO a -> ST s a

export
runST : (forall s . ST s a) -> a
runST p
    = let MkST prog = p {s = ()} in -- anything will do :)
          unsafePerformIO prog

mutual
  export
  Functor (ST s) where
    map fn st = pure $ fn !st

  export
  Applicative (ST s) where
    pure = MkST . pure
    (<*>) f a = pure $ !f !a

  export
  Monad (ST s) where
    MkST p >>= k
        = MkST $ do p' <- p
                    let MkST kp = k p'
                    kp

export
newSTRef : a -> ST s (STRef s a)
newSTRef val
    = MkST $ do r <- newIORef val
                pure (MkSTRef r)

%inline
export
readSTRef : STRef s a -> ST s a
readSTRef (MkSTRef r) = MkST $ readIORef r

%inline
export
writeSTRef : STRef s a -> (val : a) -> ST s ()
writeSTRef (MkSTRef r) val = MkST $ writeIORef r val

export
modifySTRef : STRef s a -> (a -> a) -> ST s ()
modifySTRef ref f
    = do val <- readSTRef ref
         writeSTRef ref (f val)


text:
-- Matrix.idr
--
-- Matrix arithmetics with dependent types

module Matrix

import Data.Vect

-- matrix addition
addMatrix : Num numType =>
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType)

-- matrix multiplication
multMatrix : Num numType =>
             Vect n (Vect m numType) ->
             Vect m (Vect p numType) ->
             Vect n (Vect p numType)

-- transpose matrix
createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) ->
                  Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                             transposeHelper x xsTrans

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Control.Comonad

import Control.Monad.Identity

import Data.List1
import Data.Morphisms
import Data.Stream

%default total

--------------------------------------------------------------------------------
--          Comonad
--------------------------------------------------------------------------------

public export
interface Functor w => Comonad w where
  extract   : w a -> a

  duplicate : w a -> w (w a)
  duplicate = extend id

  extend    : (w a -> b) -> w a -> w b
  extend f = map f . duplicate

--------------------------------------------------------------------------------
--          Comonad Implementations
--------------------------------------------------------------------------------

public export
Comonad (Pair e) where
  extract         = snd
  duplicate (e,a) = (e, (e, a))

public export
Comonad Identity where
  extract   = runIdentity
  duplicate = Id

public export
Comonad Stream where
  extract               = head
  duplicate xs@(_ :: t) = xs :: duplicate t

public export
Comonad List1 where
  extract = head
  duplicate (x ::: xs) = (x ::: xs) ::: tails xs
    where tails : List a -> List (List1 a)
          tails []        = []
          tails (x :: xs) = (x ::: xs) :: tails xs

public export
Monoid e => Comonad (Morphism e) where
  extract   (Mor f) = f neutral
  duplicate (Mor f) = Mor $ \e => Mor (\e' => f (e <+> e'))

--------------------------------------------------------------------------------
--          ComonadApply
--------------------------------------------------------------------------------

infixl 4 <@, @>, <@@>, <@>

public export
interface Comonad w => ComonadApply w where
  (<@>) : w (a -> b) -> w a -> w b

  (@>)  : w a -> w b -> w b
  (@>) = flip (<@)

  (<@) : w a -> w b -> w a
  a <@ b = map const a <@> b

--------------------------------------------------------------------------------
--          ComonadApply Implementations
--------------------------------------------------------------------------------

public export
Semigroup m => ComonadApply (Pair m) where
  (m, f) <@> (n, a) = (m <+> n, f a)
  (m, a) <@  (n, _) = (m <+> n, a)
  (m, _)  @> (n, b) = (m <+> n, b)

public export
ComonadApply List1 where
  (<@>) = (<*>)

public export
ComonadApply Stream where
  (<@>) = (<*>)

public export
Monoid m => ComonadApply (Morphism m) where
  (<@>) = (<*>)

public export
ComonadApply Identity where
  (<@>) = (<*>)
  _ @> b = b
  b <@ _ = b

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

infixl 1 =>>
infixr 1 <<=, =<=, =>=

||| `extend` with the arguments swapped. Dual to `>>=` for a `Monad`.
public export %inline
(=>>) : Comonad w => w a -> (w a -> b) -> w b
(=>>) = flip extend

||| `extend` in operator form
public export %inline
(<<=) : Comonad w => (w a -> b) -> w a -> w b
(<<=) = extend

||| Right-to-left `Cokleisli` composition
public export %inline
(=<=) : Comonad w => (w b -> c) -> (w a -> b) -> w a -> c
f =<= g = f . extend g

||| Left-to-right `Cokleisli` composition
public export %inline
(=>=) : Comonad w => (w a -> b) -> (w b -> c) -> w a -> c
f =>= g = g . extend f

||| Flipped version of `<@>`.
public export %inline
(<@@>) : ComonadApply w => w a -> w (a -> b) -> w b
(<@@>) = flip (<@>)


text:
import Data.SnocList

A, B, C, D, E : SnocList Nat
A = [<]

B = Lin :< 1 :< 2 :< 3

C = [< 1, 2, 3]

D = [< 1, 2, 3] :< 4

E = [< 1, 2, 3] <>< [4, 5, 6]

X : List Nat
X = [< 1, 2, 3] <>> [> 4, 5, 6]

StaticTest1 : B = C
StaticTest1 = Refl

StaticTest2 : E <>> [] = X
StaticTest2 = Refl

DynamicTest1  ,
DynamicTest2 : Bool
DynamicTest1 = B == C
DynamicTest2 = (E <>> []) == X

S1,S2,S3 : String
S1 = show A
S2 = show B
S3 = show C


text:
> module Fraction.Normalize

> import Fraction.Fraction
> import Fraction.BasicOperations
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Nat.Positive
> import Nat.GCD
> import Nat.GCDOperations
> import Nat.Divisor
> import Nat.DivisorOperations
> import Nat.DivisorProperties
> import Nat.GCDAlgorithm

> %default total
> %access public export

> ||| Reduction to normal form via gcdAlg (NatGCDAlgorithm)
> normalize : Fraction -> Fraction
> normalize (m, d') = (qmg, fromNat qdg zLTqdg) where
>   d       :  Nat
>   d       =  toNat d'
>   g       :  Nat
>   g       =  gcdAlg m d
>   prf     :  (GCD g m d)
>   prf     =  gcdAlgLemma m d
>   gDm     :  (g `Divisor` m)
>   gDm     =  gcdDivisorFst prf
>   gDd     :  (g `Divisor` d)
>   gDd     =  gcdDivisorSnd prf
>   qmg     :  Nat
>   qmg     =  quotient m g gDm
>   qdg     :  Nat
>   qdg     =  quotient d g gDd
>   zLTd    :  (Z `LT` d)
>   zLTd    =  toNatLTLemma d'
>   zLTqdg  :  (Z `LT` qdg)
>   zLTqdg  =  quotientPreservesPositivity d g gDd zLTd
> -- %freeze normalize

> {-
> ||| Reduction to normal form via gcdAlg (NatGCDAlgorithm)
> normalize : Fraction -> Fraction
> normalize (m, d') =
>   let d       :  Nat
>               =  toNat d' in
>   let g       :  Nat
>               =  gcdAlg m d in
>   let prf     :  (GCD g m d)
>               =  gcdAlgLemma m d in
>   let gDm     :  (g `Divisor` m)
>               =  gcdDivisorFst prf in
>   let gDd     :  (g `Divisor` d)
>               =  gcdDivisorSnd prf in
>   let qmg     :  Nat
>               =  quotient m g gDm in
>   let qdg     :  Nat
>               =  quotient d g gDd in
>   let zLTd    :  (Z `LT` d)
>               =  toNatLTLemma d' in
>   let zLTqdg  :  (Z `LT` qdg)
>               =  quotientPreservesPositivity d g gDd zLTd in
>   (qmg, fromNat qdg zLTqdg)
> -- %freeze normalize
> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module VQE

import Data.Nat
import Data.Vect
import Unitary
import Control.Linear.LIO
import Lemmas
import QStateT
import Injection
import LinearTypes
import Complex
import System.Random
import QuantumOp
import RandomUtilities

%default total

-- Example of code where quantum and classical information interact
-- The VQE (Variational Quantum Eigensolver) algorithm finds the lowest eigenvalue for an Hamiltonian operator
-- More precisely, we suppose that the eigenstate corresponding to the lowest eigenvalue is given by some ansatz
-- that depends on some parameters, and we optimize the value of the parameters, to find the eigenvalue.

-- The next lines of code explain how the ansatz is given in general. The ansatz has some depth p, and all parameters
-- the ansatz is depending on are given by two matrices of angles, represented by the RotationAnglesMatrix type.

||| Type for the matrices of rotation angles
|||
||| Matrix of size (n+1) * m
public export
RotationAnglesMatrix : Nat -> Nat -> Type
RotationAnglesMatrix n m = Vect (S n) (Vect m Double)

||| Unitary operator used for linear entanglement
|||
||| n -- The arity of the operator
export
linearEntanglement : (n : Nat) -> Unitary n
linearEntanglement 0 = IdGate
linearEntanglement 1 = IdGate
linearEntanglement (S (S n)) =
  let circ = IdGate {n = 1} # linearEntanglement (S n)
  in circ . (CNOT 0 1 IdGate)

||| Unitary operator, tensor product of phase gates
|||
||| n      -- The arity of the operator
||| phases -- The vector of phases
tensorRzs : {n : Nat} -> (phases : Vect n Double) -> Unitary n
tensorRzs phases = tensorMapSimple (map (\phase => RzGate phase) phases)

||| Unitary operator, tensor product of Ry gates
|||
||| n      -- The arity of the operator
||| phases -- The vector of phases for the Ry gates
tensorRys : {n : Nat} -> (phases : Vect n Double) -> Unitary n
tensorRys phases = tensorMapSimple (map (\phase => RyGate phase) phases)

||| The overall unitary operator for VQE, the ansatz
|||
||| n        -- The arity of the operator
||| depth    -- The depth of the ansatz, i.e. the number of repetitions of the pattern
||| phasesRy -- The vector of phases for all the Ry rotations
||| phasesRz -- The vector of phases for all the phase gates
||| output   -- The overall unitary operator for VQE, the ansatz
export
ansatz : (n : Nat) -> (depth : Nat) ->
         (phasesRy : RotationAnglesMatrix depth n) ->
         (phasesRz : RotationAnglesMatrix depth n) ->
         Unitary n
ansatz n 0 [phaseRy] [phaseRz] = tensorRzs phaseRz . tensorRys phaseRy
ansatz n (S d) (phaseRy :: phasesRy) (phaseRz :: phasesRz) =
  let circ1 = ansatz n d phasesRy phasesRz
  in circ1 . linearEntanglement n . tensorRzs phaseRz . tensorRys phaseRy

------------- THE HAMILTONIAN -------------------------------------------------------

-- The ansatz gives us some vector |psi>, that depends on some parameters
-- We want to find the minimum value of <psi|H|psi> over all possible parameters
-- To do that, we need a way to compute <psi|H|psi>.

-- This is easy if H is an tensor product of Pauli Matrices. In this case, one can build a circuit U_H
-- such that, if we build the circuit U_H|psi> and measure the first qubit, then
-- <psi|H|psi> is equal to x - y where x (resp.y) is the probability of measuring 0 (resp. 1)

-- More generally, if H is a sum of tensor product of Pauli Matrices, say H = a_1 H_1 + ... a_k H_k
-- then one can obtain <psi|H|psi> by computing separately each <psi|H_i|psi> using the previous idea

-- As a consequence, for all intent and purposes here, we suppose that Hamiltonians are given by linear combinations of
-- tensor product of Pauli Matrices.
-- This is represented by the type Hamiltonian below, that is a list of pairs (coefficient, tensor product of pauli matrix)

||| Data type for the the Pauli matrices X,Y,Z and Identity
public export
data PauliAtomic : Type where
  PauliI : PauliAtomic
  PauliX : PauliAtomic
  PauliY : PauliAtomic
  PauliZ : PauliAtomic

||| Tensor product of n Pauli matrices represented as a vector
||| n -- number of qubits
public export
PauliBasis : Nat -> Type
PauliBasis n = Vect n PauliAtomic

||| Decomposition of Hamiltonian as sum of Pauli matrices
||| Hamiltonian = a_1P_1 + a_2P_2 + ... + a_kP_k
||| n -- number of qubits
public export
Hamiltonian : Nat -> Type
Hamiltonian n = List (Double, PauliBasis n)

-- Now the next lines of code  explain how to obtain the  value of <psi|H|psi>, first for a tensor product of Pauli matrices, then more generally.

-- First here is the definition of U_H, the unitary s.t. measuring U_H|psi> makes us able to compute <psi|H|psi>:

--------------------- COMPUTE THE ENERGY ------------------------------

-- The value of the energy <psi|H|psi> can be computed by applying a unitary operator U_H to |psi> and mesuring the first qubit
-- Here the operator U_H uses one more  qubits than H. It is possible to use the exact same number of qubits, but the code is easier this way.

||| With a tensor product of Pauli matrices, compute the corresponding unitary operator U_H
|||
||| n      -- number of qubits
||| h      -- vector that represents the tensor product of Pauli matrices
||| output -- U_h
encodingUnitary : {n : Nat} -> (h : PauliBasis n) -> Unitary (S n)
encodingUnitary [] = IdGate
encodingUnitary {n = S k} (PauliI :: xs) = rewrite sym $ lemmaplusOneRight k in (encodingUnitary xs) # IdGate {n=1}
encodingUnitary {n = S k} (PauliX :: xs) =
  let p1 = lemmakLTSk k
  in rewrite sym $ lemmaplusOneRight k in CNOT (S k) 0 (H (S k) ((encodingUnitary xs) # IdGate {n=1}))
encodingUnitary {n = S k} (PauliY :: xs) =
  let p1 = lemmakLTSk k
  in rewrite sym $ lemmaplusOneRight k in CNOT (S k) 0 (H (S k) (S (S k) ((encodingUnitary xs) # IdGate {n=1})))
encodingUnitary {n = S k} (PauliZ :: xs) =
  let p1 = lemmakLTSk k
  in rewrite sym $ lemmaplusOneRight k in CNOT (S k) 0 ((encodingUnitary xs) # IdGate {n=1})

-- the next function computes <psi|H|psi>, for H a tensor product of Pauli Matrices
-- This is the function that needs to run the quantum circuit
-- As explained above, to obtain <psi|H|psi>, we produce a circuit for U_H|psi> and then measure the first qubit
-- The value of <psi|H|psi> is then equal to the probability of measuring 0 minus the probability of measuring 1
-- the following code runs the whole experiment nSamples times,
-- and records the number of time we measure 0 and the number of times we measure 1 and returns the difference between the two quantities
-- if nSamples is big enough, then <psi|H|psi> is therefore well approximated by the result of this function divided by the number of samples.

||| Computes an approximation of <psi|H|psi> when H is a tensor product of Pauli Matrices
||| More precisely, <psi|H|psi> is equal to the result of this function divided by nSamples
|||
||| n        -- number of qubits
||| p        -- tensor product of Pauli matrices
||| nSamples -- the number of time we sample
||| circuit  -- the state |psi>
||| output   -- computed energy
computeEnergyPauli : QuantumOp t => (n : Nat) -> (p : PauliBasis n) -> (nSamples : Nat) -> (circuit : Unitary n) -> IO Double
computeEnergyPauli n p 0 circuit = pure 0
computeEnergyPauli n p (S nSamples) circuit = do
  let encodingCircuit = encodingUnitary p
  (b :: _) <- run (do
               qs <- newQubits {t} (S n)
               qs <- applyUnitary qs ( (IdGate {n=1}) # circuit)
               qs <- applyUnitary qs encodingCircuit
               measureAll qs
               )
  rest <- computeEnergyPauli {t} n p nSamples circuit
  if (not b) then pure $ 1 + rest else pure $ rest - 1

-- the next function computes <psi|H|psi> for a general hamiltonian H, expressed as a linear combination of tensor product of Pauli Matrices
-- we just have to call the function computeEnergyPauli for each element inside the linear combination:

||| Compute an approximation of <psi|H|psi> for a general Hamiltonian H
|||
||| n        -- number of qubits
||| h        -- the hamiltonian of the problem
||| nSamples -- the number of time we sample for each component of H
||| circuit  -- the state |psi>
||| output   -- computed energy
computeEnergy : QuantumOp t => (n : Nat) -> (h : Hamiltonian n) -> (nSamples : Nat) -> (circuit : Unitary n) -> IO Double
computeEnergy n [] nSamples circuit = pure 0
computeEnergy n ((r, p) :: hs) nSamples circuit = do
  res1 <- computeEnergy {t} n hs nSamples circuit
  res2 <- computeEnergyPauli {t} n p nSamples circuit
  pure $ res1 + r*res2/(cast nSamples)

--------------------- CLASSICAL OPTIMISATION ------------------------

--- The energy that is compute by the function computeEnergy is fed to the function classicalOptimisation before
--- That will produces  new parameters for the ansatz to try, based on the value of <psi|H|psi> on all previous runs

--- This function should use general optimisation techniques, like for instance the Nelder-Mead method
--- For simplicity, we opted instead for a function that returns random parameters

||| Generate a matrix of size (n+1) * m of random Double
export
randomMatrix : (n : Nat) -> (m : Nat) -> IO (RotationAnglesMatrix n m)
randomMatrix 0 m = do
  xs <- randomVect m
  pure [xs]
randomMatrix (S n) m = do
  xs <- randomVect m
  ys <- randomMatrix n m
  pure (xs :: ys)

||| The (probabilistic) classical optimisation procedure for VQE.
||| IO output allows us to use probabilistic optimisation procedures.
||| Given all previously observed information, determine new rotation angles for the next VQE run.
||| We ask for the function to be able to return also parameters for the very first ansatz (that is, the function
||| will be called for the first time with an empty vector of previous information)
||| Remark: we randomly generate the next rotation angles for simplicity.
|||
||| k             -- number of previous iterations of the algorithm
||| n             -- arity of the ansatz circuit
||| depth         -- depth of the ansatz circuit
||| h             -- hamiltonian of the problem
||| previous_info -- previously used parameters and measurement outcomes
||| output        -- new rotation angles for the next run of VQE
classicalOptimisation : {n : Nat} -> (depth : Nat) ->
                        (h : Hamiltonian n) ->
                        (previous_info : Vect k (RotationAnglesMatrix depth n, RotationAnglesMatrix depth n, Double)) ->
                        IO (RotationAnglesMatrix depth n, RotationAnglesMatrix depth n)
classicalOptimisation depth h previous_info = do
  phasesRy <- randomMatrix depth n
  phasesRz <- randomMatrix depth n
  pure (phasesRy, phasesRz)

-----------------------PUTTING QUANTUM AND CLASSICAL PARTS TOGETHER -------------------------

-- We now put everything together
-- This function will run the whole process k times, computing <psi|H|psi> at each step, and calling the classical optimiser to obtain
-- the next value of |psi> to test

||| Helper function for VQE
||| n        -- number of qubits
||| h        -- the hamiltonian of the problem
||| nSamples -- number of times we sample to compute <psi|H|psi>
||| k        -- number of iterations of the algorithm
||| depth    -- depth of the ansatz circuit
||| output   -- all observed information : rotation angles and computed energies
VQE': QuantumOp t =>
       (n : Nat) -> (h : Hamiltonian n) -> (nSamples : Nat) -> (k : Nat) -> (depth : Nat) ->
       IO (Vect k (RotationAnglesMatrix depth n, RotationAnglesMatrix depth n, Double))
VQE' n h nSamples 0 depth = pure []
VQE' n h nSamples (S k) depth = do
  previous_info <- VQE' {t} n h nSamples k depth
  (phasesRy, phasesRz) <- classicalOptimisation depth h previous_info
  let circuit = ansatz n depth phasesRy phasesRz
  energy <- computeEnergy {t} n h nSamples circuit
  pure $ (phasesRy, phasesRz, energy) :: previous_info

--- The VQE algorithm just calls the previous function, and returns the minimum value of <psi|H|psi> that was observed
--- Note that, in practice, if the classical Optimiser does their job correctly, the minimum value of <psi|H|psi>
--- is very likely to be obtained in the last iteration. As we use a random function instead of an optimiser, this is
--- not true, so we take the minimum among all runs.

||| VQE algorithm
||| n        -- number of qubits
||| h        -- the hamiltonian of the problem
||| nSamples -- number of times we sample to compute <psi|H|psi>
||| k        -- number of iterations of the algorithm
||| depth    -- depth of the ansatz circuit
||| output   -- the lowest computed energy
export
VQE : QuantumOp t =>
      (n : Nat) -> (h : Hamiltonian n) -> (nSamples : Nat) -> (k : Nat) -> (depth : Nat) ->
      IO Double
VQE n h nSamples k depth = do
  observed_info <- VQE' {t=t} n h nSamples (S k) depth
  let energies = map (\(_, _, r) => r) observed_info
  pure $ foldl min (head energies) energies

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Rhone.Canvas.Transformation

import JS
import Rhone.Canvas.Angle
import Web.Html

--------------------------------------------------------------------------------
--          Transformation
--------------------------------------------------------------------------------

public export
data Transformation : Type where
  Id        : Transformation
  Transform : (a,b,c,d,e,f : Double) -> Transformation

export
scale : (h,w : Double) -> Transformation
scale h w = Transform h 0 0 w 0 0

export
rotate : Angle -> Transformation
rotate phi =
  let r = toRadians phi
      c = cos r
      s = sin r
   in Transform c s (-s) c 0 0

export
translate : (dx,dy : Double) -> Transformation
translate dx dy = Transform 0 0 0 0 dx dy

export
mult : Transformation -> Transformation -> Transformation
mult Id x  = x
mult x  Id = x
mult (Transform a1 b1 c1 d1 e1 f1) (Transform a2 b2 c2 d2 e2 f2) =
  Transform (a1 * a2 + c1 * b2)
            (b1 * a2 + d1 * b2)
            (a1 * c2 + c1 * d2)
            (b1 * c2 + d1 * d2)
            (a1 * e2 + c1 * f2 + e1)
            (b1 * e2 + d1 * f2 + f1)

export %inline
Semigroup Transformation where
  (<+>) = mult

export %inline
Monoid Transformation where
  neutral = Id

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

export
apply : CanvasRenderingContext2D -> Transformation -> JSIO ()
apply ctxt Id                      = pure ()
apply ctxt (Transform a b c d e f) = setTransform ctxt a b c d e f


text:
-- The regression that this tests for is defunct unsafePerformIO

io : IO Int
io = pure 42

main : IO ()
main = printLn $ unsafePerformIO io

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:
import Elem
import ElemBool
import ElemType
import Hangman
import RemoveElem


text:
module Adithyau.Odds

import Evens

import Intro

data IsOdd : Nat -> Type where
	OneOdd : IsOdd (S Z)
	SSOdd : (k : Nat) -> IsOdd k -> IsOdd (S (S k))

threeOdd : IsOdd 3				{- 3 is odd -}
threeOdd = SSOdd (S Z) OneOdd

twoNotOdd : IsOdd 2 -> Void		{- 2 is not odd -}
twoNotOdd OneOdd impossible
twoNotOdd (SSOdd _ _) impossible

ifOddSEven : (n : Nat) -> (IsOdd n) -> (IsEven (S n))				{- if n is odd, S n is even -}
ifOddSEven (S Z) OneOdd = SSEven 0 ZEven
ifOddSEven (S (S k)) (SSOdd k x) = SSEven (S k) (ifOddSEven k x)

ifEvenSOdd : (n : Nat) -> (IsEven n) -> (IsOdd (S n))				{- if n is even, S n is odd -}
ifEvenSOdd Z ZEven = OneOdd
ifEvenSOdd (S (S k)) (SSEven k x) = SSOdd (S k) (ifEvenSOdd k x)

nOddorEven : (n : Nat) -> Either (IsEven n) (IsOdd n)				{- n is odd or even -}
nOddorEven Z = Left ZEven
nOddorEven (S k) = case (nOddorEven k) of
						(Left l) => Right (ifEvenSOdd k l)
						(Right r) => Left (ifOddSEven k r)

nNotOddandEven : (n : Nat) -> (IsEven n) -> (IsOdd n) -> Void		{- n is not both odd and even -}
nNotOddandEven Z ZEven _ impossible
nNotOddandEven Z (SSEven _ _) _ impossible
nNotOddandEven (S Z) _ OneOdd  impossible
nNotOddandEven (S Z) _ (SSOdd _ _) impossible
nNotOddandEven (S (S k)) ZEven _ impossible
nNotOddandEven (S (S k)) (SSEven k x) OneOdd impossible
nNotOddandEven (S (S k)) (SSEven k x) (SSOdd k y) = nNotOddandEven k x y

isEvenAdd : (n : Nat) -> (m : Nat) -> (IsOdd n) -> (IsOdd m) -> (IsEven (add n m))				{- if n and m are odd, add n m is even -}
isEvenAdd (S Z) k OneOdd x = ifOddSEven k x
isEvenAdd (S (S k)) l (SSOdd k proofk) proofl = SSEven (add k l) (isEvenAdd k l proofk proofl)

isDoubleS : (n : Nat) -> (IsOdd n) -> (m : Nat ** n = S (double m))					{- if n is odd, there exists an m such that n = S (double m) -}
isDoubleS (S Z) OneOdd = (Z ** Refl)
isDoubleS (S (S k)) (SSOdd k x) = step where
	step = case (isDoubleS k x) of
				(m ** pf) => ((S m) ** apNat (\l => S (S l)) k (S (double m)) pf)