text:
module HoareAssertAssume

import Assn
import Expr
import Logic
import Maps

%access public export

%default total

data Com : Type where
  CSkip : Com
  CAss : Id -> AExp -> Com
  CSeq : Com -> Com -> Com
  CIf : BExp -> Com -> Com -> Com
  CWhile : BExp -> Com -> Com
  CAssert : BExp -> Com
  CAssume : BExp -> Com

infix 5 ::=

SKIP : Com
SKIP = CSkip

(::=) : Id -> AExp -> Com
(::=) = CAss

(>>=) : Com -> (() -> Com) -> Com
(>>=) c f = CSeq c (f ())

syntax IFB [b] THEN [c1] ELSE [c2] FI = CIf b c1 c2

WHILE : BExp -> Com -> Com
WHILE = CWhile

ASSERT : BExp -> Com
ASSERT = CAssert

ASSUME : BExp -> Com
ASSUME = CAssume

data Result : Type where
  RNormal : State -> Result
  RError : Result

rNormalInjective : RNormal st1 = RNormal st2 -> st1 = st2
rNormalInjective Refl = Refl

Uninhabited (RError = RNormal st) where
  uninhabited Refl impossible

data CEval : Com -> State -> Result -> Type where
  E_Skip : CEval CSkip st (RNormal st)
  E_Ass : aeval st a1 = n -> CEval (CAss x a1) st (RNormal (t_update x n st))
  E_SeqNormal : CEval c1 st1 (RNormal st2) -> CEval c2 st2 r ->
                CEval (CSeq c1 c2) st1 r
  E_SeqError : CEval c1 st RError -> CEval (CSeq c1 c2) st RError
  E_IfTrue : beval st b = True -> CEval c1 st r -> CEval (CIf b c1 c2) st r
  E_IfFalse : beval st b = False -> CEval c2 st r -> CEval (CIf b c1 c2) st r
  E_WhileEnd : beval st b = False -> CEval (CWhile b c) st (RNormal st)
  E_WhileLoopNormal : beval st b = True ->
                      CEval c st (RNormal st1) -> CEval (CWhile b c) st1 r ->
                      CEval (CWhile b c) st r
  E_WhileLoopError : beval st b = True -> CEval c st RError ->
                     CEval (CWhile b c) st RError
  E_AssertTrue : beval st b = True -> CEval (CAssert b) st (RNormal st)
  E_AssertFalse : beval st b = False -> CEval (CAssert b) st RError
  E_Assume : beval st b = True -> CEval (CAssume b) st (RNormal st)

syntax [c1] "/" [st1] "\\\\" [st2] = CEval c1 st1 st2

HoareTriple : (p : Assertion) -> (c : Com) -> (q : Assertion) -> Type
HoareTriple p c q = (st : State) -> (r : Result) -> (c / st \\ r) -> p st ->
                    (st' : State ** (r = RNormal st', q st'))

assert_assume_differ : DPair (Assertion, BExp, Assertion)
                             (\(p, b, q) => ( HoareTriple p (ASSUME b) q
                                            , Not (HoareTriple p (ASSERT b) q) ))
assert_assume_differ = ((const (), 0 == 1, const ()) ** (assume, not_assert))
where assume : HoareTriple (const ()) (ASSUME (0 == 1)) (const ())
      assume st (RNormal _) (E_Assume _) _ = (st ** (Refl, ()))
      not_assert : Not (HoareTriple (const ()) (ASSERT (0 == 1)) (const ()))
      not_assert ht =
        let (_ ** (prf, _)) = ht empty_state RError (E_AssertFalse Refl) ()
        in absurd prf

assert_implies_assume : (p : Assertion) -> (b : BExp) -> (q : Assertion) ->
                        HoareTriple p (ASSERT b) q -> HoareTriple p (ASSUME b) q
assert_implies_assume p b q ht st (RNormal st) (E_Assume prf) p_st =
  ht st (RNormal st) (E_AssertTrue prf) p_st

hoare_assign : (q : Assertion) -> (x : Id) -> (a : AExp) ->
               HoareTriple (AssignSub x a q) (x ::= a) q
hoare_assign q x a st _ (E_Ass {n} prf) p_st =
  let q_st = replace {P=\m => q (t_update x m st)} prf p_st
  in (t_update x n st ** (Refl, q_st))

hoare_consequence_pre : (p, p', q : Assertion) -> (c : Com) ->
                        HoareTriple p' c q -> p ->> p' -> HoareTriple p c q
hoare_consequence_pre p p' q c htc imp st r rel p_st = htc st r rel (imp st p_st)

hoare_consequence_post : (p, q, q' : Assertion) -> (c : Com) ->
                         HoareTriple p c q' -> q' ->> q -> HoareTriple p c q
hoare_consequence_post p q q' c htc imp st r rel p_st =
  let (st' ** (prf, q'_st')) = htc st r rel p_st
  in (st' ** (prf, imp st' q'_st'))

hoare_seq : (p, q, r : Assertion) -> (c1, c2 : Com) ->
            HoareTriple q c2 r -> HoareTriple p c1 q ->
            HoareTriple p (do c1; c2) r
hoare_seq p q r c1 c2 htc2 htc1 st res (E_SeqNormal {st2} cc1 cc2) p_st =
  let (st2 ** (pf, q_st2)) = htc1 st (RNormal st2) cc1 p_st
      cc2' = replace {P=\x => CEval c2 x res} (rNormalInjective pf) cc2
  in htc2 st2 res cc2' q_st2
hoare_seq p q r c1 c2 htc2 htc1 st RError (E_SeqError cc1) p_st =
  let (_ ** (prf, _)) = htc1 st RError cc1 p_st
  in absurd prf

hoare_skip : (p : Assertion) -> HoareTriple p SKIP p
hoare_skip p st (RNormal st) E_Skip p_st = (st ** (Refl, p_st))

hoare_if : (p, q : Assertion) -> (b : BExp) -> (ct, cf : Com) ->
           HoareTriple (\st => (p st, BAssn b st)) ct q ->
           HoareTriple (\st => (p st, Not (BAssn b st))) cf q ->
           HoareTriple p (CIf b ct cf) q
hoare_if p q b ct cf htct htcf st r (E_IfTrue prf cct) p_st =
  htct st r cct (p_st, prf)
hoare_if p q b ct cf htct htcf st r (E_IfFalse prf ccf) p_st =
  htcf st r ccf (p_st, bexp_eval_false prf)

hoare_while : (p : Assertion) -> (b : BExp) -> (c : Com) ->
              HoareTriple (\st => (p st, BAssn b st)) c p ->
              HoareTriple p (CWhile b c) (\st => (p st, Not (BAssn b st)))
hoare_while p b c htc st (RNormal st) (E_WhileEnd prf) p_st =
  (st ** (Refl, p_st, bexp_eval_false prf))
hoare_while p b c htc st r w@(E_WhileLoopNormal {st1} prf cc cnext) p_st =
  let (st2 ** (pf, p_st2)) = htc st (RNormal st1) cc (p_st, prf)
      cnext' = assert_smaller w
                              (replace {P=\x => CEval (CWhile b c) x r}
                                       (rNormalInjective pf) cnext)
  in hoare_while p b c htc st2 r cnext' p_st2
hoare_while p b c htc st RError (E_WhileLoopError prf cc) p_st =
  let (_ ** (pf, _)) = htc st RError cc (p_st, prf)
  in absurd pf

hoare_assert : (p : Assertion) -> (b : BExp) ->
               p ->> (\st => BAssn b st) -> HoareTriple p (ASSERT b) p
hoare_assert p b _ st (RNormal st) (E_AssertTrue prf) p_st = (st ** (Refl, p_st))
hoare_assert p b imp st RError (E_AssertFalse prf) p_st =
  absurd $ trans (sym prf) (imp st p_st)

hoare_assume : (p : Assertion) -> (b : BExp) ->
               HoareTriple p (ASSUME b) (\st => (p st, BAssn b st))
hoare_assume p b st (RNormal st) (E_Assume prf) p_st = (st ** (Refl, p_st, prf))

assert_assume_example : HoareTriple (const ())
                                    (do ASSUME (X == 1)
                                        X ::= X + 1
                                        ASSERT (X == 2))
                                    (const ())
assert_assume_example =
  let ht_assm = hoare_consequence_post
                  (const ())
                  (\st => st X = 1)
                  (\st => ((), BAssn (X == 1) st))
                  (ASSUME (X == 1))
                  (hoare_assume (const ()) (X == 1))
                  (\st, (_, prf) => fst (nat_beq_iff (st X) 1) prf)
      ht_asgn = hoare_consequence_pre
                  (\st => st X = 1)
                  (\st => st X + 1 = 2)
                  (\st => st X = 2)
                  (X ::= X + 1)
                  (hoare_assign (\st => st X = 2) X (X + 1))
                  (\st, p_st => plusConstantRight (st X) 1 1 p_st)
      ht_asrt = hoare_consequence_post
                  (\st => st X = 2)
                  (const ())
                  (\st => st X = 2)
                  (ASSERT (X == 2))
                  (hoare_assert (\st => st X = 2)
                                (X == 2)
                                (\st, prf => snd (nat_beq_iff (st X) 2) prf))
                  (\_, _ => ())
  in hoare_seq (const ())
               (\st => st X = 1)
               (const ())
               (ASSUME (X == 1))
               (do X ::= X + 1
                   ASSERT (X == 2))
               (hoare_seq (\st => st X = 1)
                          (\st => st X = 2)
                          (const ())
                          (X ::= X + 1)
                          (ASSERT (X == 2))
                          ht_asrt
                          ht_asgn)
               ht_assm


text:
module NewEden.Natural

import Prelude.Either
import public Prelude.Uninhabited

import public NewEden.Algebra
import public NewEden.NaturalAxioms
import public NewEden.NaturalPropertiesHelpers -- compiler bug #144; can't use private in types

{- Natural

   Natural p is a natural number expressed in terms of operations on a given
   set of NaturalProperties p.

   Everything else in this module is expressing the axioms given in
   NaturalProperties in terms of operations on Natural p, so now
   we can use Natural p much the same as we would the 'normal' numeric types.
-}

data Natural : NaturalProperties t -> Type where
  MkNatural : (n:NaturalProperties t) -> (a:t) -> Natural n

value : {p:NaturalProperties t} -> Natural p -> t
value {p} (MkNatural p x) = x

properties : {p:NaturalProperties t} -> Natural p -> NaturalProperties t
properties (MkNatural p _) = p

(+) : {p:NaturalProperties t} -> Natural p -> Natural p -> Natural p
(+) {p} (MkNatural p x) (MkNatural p y) =
  MkNatural p $ privatePlus p x y

(*) : {p:NaturalProperties t} -> Natural p -> Natural p -> Natural p
(*) {p} (MkNatural p x) (MkNatural p y) =
  MkNatural p $ privateMultiply p x y

{- fromInteger

   This is the first place we see the real power of an axiomatic implementation.
   Here we are able to construct arbitrary natural numbers and put them in the
   compiler's head in *logarithmic* space (rather than linear space, like the Peano Nat).
-}

fromInteger : Integer -> Natural p
fromInteger rem =
  let z = MkNatural p (zero p) in
  let o = MkNatural p (one p) in
  case rem of
    0 => z
    1 => o
    _ =>
         case (assert_total $ prim__sremBigInt rem 2) of
           0 => (o + o) * (assert_total $ fromInteger (prim__sdivBigInt rem 2))
           1 => o + (assert_total $ fromInteger (prim__subBigInt rem 1))
           _ => o -- impossible

-- force resolution of 0 to Natural p, since occasionally 0 is
-- ambiguous (e.g., right below in zeroIsNotOne)
Z : (p:NaturalProperties t) -> Natural p
Z p = 0

zeroIsNotOne : (p:NaturalProperties t) -> (Z p = 1 -> Void)
zeroIsNotOne p =
  let prf = NewEden.NaturalPropertiesHelpers.privateZeroIsNotOne p in
  (\given => prf $ equalityMap value given)

plusCommutative : (p:NaturalProperties t) -> CommutativeFunction (Natural p) (+)
plusCommutative p =
  let (MkCommutativeFunction _ prf) = NewEden.NaturalPropertiesHelpers.privatePlusCommutative p in
  MkCommutativeFunction
    (+)
    (\(MkNatural p x),(MkNatural p y) => equalityMap (MkNatural p) $ prf x y)

plusAssociative : (p:NaturalProperties t) -> AssociativeFunction (Natural p) (+)
plusAssociative p =
  let (MkMonoid af _ _ _) = NewEden.NaturalPropertiesHelpers.privatePlusMonoid p in
  let (MkAssociativeFunction _ prf) = af in
  MkAssociativeFunction
    (+)
    (\(MkNatural p x),(MkNatural p y),(MkNatural p z) => equalityMap (MkNatural p) $ prf x y z)

plusMonoid : (p:NaturalProperties t) -> NewEden.Algebra.Monoid (Natural p) (+) 0
plusMonoid P =
  let (MkMonoid _ _ p1 p2) = NewEden.NaturalPropertiesHelpers.privatePlusMonoid P in
  MkMonoid
    (plusAssociative P)
    (Z P)
    (\(MkNatural P x) => equalityMap (MkNatural P) $ p1 x)
    (\(MkNatural P x) => equalityMap (MkNatural P) $ p2 x)

plusLacksInverses : (p:NaturalProperties t) -> StrictMonoid $ NewEden.Natural.plusMonoid p
plusLacksInverses P =
  let (MkStrictMonoid _ prf) = NewEden.NaturalPropertiesHelpers.privatePlusLacksInverses P in
  MkStrictMonoid
    (plusMonoid P)
    (\(MkNatural P x),(MkNatural P y),given =>
      let given' = equalityMap value $ given in
      equalityMap (MkNatural P) $ prf x y given'
    )

plusMonomorphic : (p:NaturalProperties t) -> ((n:Natural p) -> MonomorphicFunction $ (+) n)
plusMonomorphic p =
  let g = NewEden.NaturalPropertiesHelpers.privatePlusMonomorphic p in
  (\(MkNatural p x) =>
    let (MkMonomorphicFunction _ prf) = g x in
    MkMonomorphicFunction
      ((+) (MkNatural p x))
      (\(MkNatural p y),(MkNatural p z),given =>
        equalityMap (MkNatural p) $ prf y z (equalityMap value given)
      )
  )

multiplyCommutative : (p:NaturalProperties t) -> CommutativeFunction (Natural p) (*)
multiplyCommutative p =
  let (MkCommutativeFunction _ prf) = NewEden.NaturalPropertiesHelpers.privateMultiplyCommutative p in
  MkCommutativeFunction
    (*)
    (\(MkNatural p x),(MkNatural p y) => equalityMap (MkNatural p) $ prf x y)

multiplyAssociative : (p:NaturalProperties t) -> AssociativeFunction (Natural p) (*)
multiplyAssociative p =
  let (MkMonoid af _ _ _) = NewEden.NaturalPropertiesHelpers.privateMultiplyMonoid p in
  let (MkAssociativeFunction _ prf) = af in
  MkAssociativeFunction
    (*)
    (\(MkNatural p x),(MkNatural p y),(MkNatural p z) => equalityMap (MkNatural p) $ prf x y z)

multiplyMonoid : (p:NaturalProperties t) -> NewEden.Algebra.Monoid (Natural p) (*) 1
multiplyMonoid P =
  let (MkMonoid _ _ p1 p2) = NewEden.NaturalPropertiesHelpers.privateMultiplyMonoid P in
  MkMonoid
    (multiplyAssociative P)
    1
    (\(MkNatural P x) => equalityMap (MkNatural P) $ p1 x)
    (\(MkNatural P x) => equalityMap (MkNatural P) $ p2 x)

multiplyLacksInverses : (p:NaturalProperties t) -> StrictMonoid $ NewEden.Natural.multiplyMonoid p
multiplyLacksInverses P =
  let (MkStrictMonoid _ prf) = NewEden.NaturalPropertiesHelpers.privateMultiplyLacksInverses P in
  MkStrictMonoid
    (multiplyMonoid P)
    (\(MkNatural P x),(MkNatural P y),given =>
      let given' = equalityMap value $ given in
      equalityMap (MkNatural P) $ prf x y given'
    )

multiplyMonomorphic : (p:NaturalProperties t) -> ((n:Natural p) -> MonomorphicFunction $ (*) n)
multiplyMonomorphic p =
  let g = NewEden.NaturalPropertiesHelpers.privateMultiplyMonomorphic p in
  (\(MkNatural p x) =>
    let (MkMonomorphicFunction _ prf) = g x in
    MkMonomorphicFunction
      ((*) (MkNatural p x))
      (\(MkNatural p y),(MkNatural p z),given =>
        equalityMap (MkNatural p) $ prf y z (equalityMap value given)
      )
  )

multiplyByZeroIsZero : (p:NaturalProperties t) -> ((a:(Natural p)) -> a * 0 = 0)
multiplyByZeroIsZero P =
  let prf = NewEden.NaturalPropertiesHelpers.privateMultiplyByZero P in
  (\(MkNatural P x) => equalityMap (MkNatural P) $ prf x)

multiplyDistributive : (p:NaturalProperties t) -> ((a:Natural p) -> (b:Natural p) -> (c:Natural p) -> a * (b + c) = (a * b) + (a * c))
multiplyDistributive p =
  let prf = NewEden.NaturalPropertiesHelpers.privateDistributiveProperty p in
  (\(MkNatural p x),(MkNatural p y),(MkNatural p z) =>
    equalityMap (MkNatural p) $ prf x y z
  )

naturalNoNumbersBetweenZeroAndOne : (p:NaturalProperties t) -> ((a:Natural p) -> (b:Natural p) -> (p1:(a = 0 -> Void)) -> (p2: a + b = 1) -> a = 1)
naturalNoNumbersBetweenZeroAndOne P =
  let lemmaSequence = NewEden.NaturalPropertiesHelpers.privateSequenceProperty P in
  (\(MkNatural P x),(MkNatural P y),given1,given2 =>
    let given1' = (\lemma => given1 $ equalityMap (MkNatural P) lemma) in
    let given2' = equalityMap value given2 in
    equalityMap (MkNatural P) $ lemmaSequence x y given1' given2'
  )

data LessThan : (a:Natural p) -> (b:Natural p) -> Type where
  MkLessThan : (a:Natural p) -> (b:Natural p) -> (c ** ((a + c = b), (c = 0 -> Void))) -> LessThan a b

data Trichotomy : (a:Type) -> (b:Type) -> (c:Type) -> Type where
  Left : {a:Type} -> {b:Type} -> {c:Type} -> (x:a) -> Trichotomy a b c
  Middle : {a:Type} -> {b:Type} -> {c:Type} -> (x:b) -> Trichotomy a b c
  Right : {a:Type} -> {b:Type} -> {c:Type} -> (x:c) -> Trichotomy a b c

compare : ((a:Natural p) -> (b:Natural p) -> Trichotomy (LessThan a b) (a = b) (LessThan b a))
compare (MkNatural p x) (MkNatural p y) =
  let prf = NewEden.NaturalPropertiesHelpers.privateCompare p in
  case prf x y of
    Left h => Middle $ equalityMap (MkNatural p) h
    Right r => case r of
      Left (c**(h,prf')) =>
        let lt = MkLessThan (MkNatural p x) (MkNatural p y) in
        Left $ lt ((MkNatural p c) ** ((equalityMap (MkNatural p) h),
                  (\prf'' => prf' $ equalityMap value prf'')))
      Right (c**(r,prf')) =>
        let lt = MkLessThan (MkNatural p y) (MkNatural p x) in
        Right $ lt ((MkNatural p c) ** ((equalityMap (MkNatural p) r),(\prf'' => prf' $ equalityMap value prf'')))

(-) : (a:Natural p) -> (b:Natural p) -> {auto prf:((LessThan a b) -> Void)} -> Natural p
(-) {prf} a b = case compare a b of
  Left x => absurd (prf x)
  Middle _ => 0
  Right (MkLessThan _ _ (c ** _)) => c

ext: idr

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module Js.Array

import Control.Monad.Syntax
import Data.Foldable.Extras
import Js
import Js.Object

%default total
%access export

public export
interface ArrayValue a where
    getAt : Class o => (index : Nat) -> (object : o) -> JS_IO a
    setAt : Class o => (index : Nat) -> (value : a) -> (object : o) -> JS_IO ()

public export
data Array = MkArray Ptr

Class Array where
    ptr (MkArray p) = p

%inline
empty : JS_IO Array
empty = MkArray <$> js "[]" (JS_IO Ptr)

%inline
length : (array : Array) -> JS_IO Nat
length = js "%0.length" (Ptr -> JS_IO Int) . ptr >=> pure . cast

%inline
append : ArrayValue a => (value : a) -> (array : Array) -> JS_IO ()
append value array = setAt !(length array) value array

createWith : Foldable f => (append' : a -> Array -> JS_IO ()) -> (source : f a) -> JS_IO Array
createWith append' source = do array <- empty
                               iter (flip append' array) source
                               pure array

%inline
create : (Foldable f, ArrayValue a) => (source : f a) -> JS_IO Array
create = createWith append

ArrayValue Bool where
    getAt index object = pure $ !(js "%1[%0] + 0" (Int -> Ptr -> JS_IO Int) (cast index) (ptr object)) /= 0
    setAt index False = js "%1[%0] = false" (Int -> Ptr -> JS_IO ()) (cast index) . ptr
    setAt index True = js "%1[%0] = true" (Int -> Ptr -> JS_IO ()) (cast index) . ptr

ArrayValue Nat where
    getAt index = jsGet (Int -> Ptr -> JS_IO Int) (cast index) . ptr >=> pure . cast
    setAt index value = jsSet (Int -> Int -> Ptr -> JS_IO ()) (cast index) (cast value) . ptr

ArrayValue Int where
    getAt index = jsGet (Int -> Ptr -> JS_IO Int) (cast index) . ptr
    setAt index value = jsSet (Int -> Int -> Ptr -> JS_IO ()) (cast index) value . ptr

ArrayValue Double where
    getAt index = jsGet (Int -> Ptr -> JS_IO Double) (cast index) . ptr
    setAt index value = jsSet (Int -> Double -> Ptr -> JS_IO ()) (cast index) value . ptr

ArrayValue String where
    getAt index = jsGet (Int -> Ptr -> JS_IO String) (cast index) . ptr
    setAt index value = jsSet (Int -> String -> Ptr -> JS_IO ()) (cast index) value . ptr

ArrayValue Ptr where
    getAt index = jsGet (Int -> Ptr -> JS_IO Ptr) (cast index) . ptr
    setAt index value = jsSet (Int -> Ptr -> Ptr -> JS_IO ()) (cast index) value . ptr

ArrayValue Object where
    getAt index = jsGet (String -> Ptr -> JS_IO Ptr) (cast index) . ptr >=> pure . MkObject
    setAt index value = jsSet (String -> Ptr -> Ptr -> JS_IO ()) (cast index) (ptr value) . ptr

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module Main
import Data.Vect

v : Vect 3 Double
v = [1, 2, 3]

main : IO ()
main = printLn v


text:
-- Taken from https://www.reddit.com/r/Idris/comments/hngthh/why_idris_need_type_definition/

record Person where
    constructor MkPerson
    firstName, middleName, lastName : String
    age : Int

fred : ? -- Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Printf

import Prelude
import Data.String

data Arg
    = AInt      Arg
    | AOther    Char Arg
    | AEnd

buildArg : List Char -> Arg
buildArg fmt = case fmt of
    '%' :: 'i' :: fmtTail   => AInt (buildArg fmtTail)
    c :: fmtTail            => AOther c (buildArg fmtTail)
    Nil                     => AEnd

argToType : Arg -> Type -> Type
argToType a result = case a of
    AInt fmtTail      => Int -> argToType fmtTail result
    AOther _ fmtTail  => argToType fmtTail result
    AEnd              => result

-- PrintfType "foo" result = result
-- PrintfType "%i\n" result = Int -> result
-- etc
PrintfType : String -> Type -> Type
PrintfType fmt result = argToType (buildArg (unpack fmt)) result

sprintf : (fmt : String) -> PrintfType fmt String
sprintf fmt = go "" (buildArg (unpack fmt)) where
    go : String -> (arg : Arg) -> argToType arg String
    go strTail arg = case arg of
        AInt fmtTail        => \i : Int => go (strTail ++ show i) fmtTail
        AOther c fmtTail    => go (strTail ++ singleton c) fmtTail
        AEnd                => strTail

test : ?result
test = sprintf "%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i%i"


text:
module Network.TLS.Certificate

import Network.TLS.Parse.DER
import Network.TLS.Parse.PEM
import Network.TLS.Parsing
import Network.TLS.Signature
import Utils.Misc
import Utils.Bytes
import Utils.IPAddr
import Data.List
import Data.Vect
import Data.Bits
import Data.String.Parser
import Data.String.Extra
import Crypto.Hash
import Decidable.Equality
import Generics.Derive

%language ElabReflection

public export
data AttributeType : Type where
  CommonName : AttributeType
  Organization : AttributeType
  OrganizationUnit : AttributeType
  Country : AttributeType
  StateOrProvince : AttributeType
  LocalityName : AttributeType
  SerialNumber : AttributeType
  UnknownAttr : List Nat -> AttributeType

%runElab derive "AttributeType" [Generic, Meta, Eq]

public export
Show AttributeType where
  show CommonName       = "CN"
  show Organization     = "O"
  show OrganizationUnit = "OU"
  show Country          = "C"
  show StateOrProvince  = "ST"
  show LocalityName     = "L"
  show SerialNumber     = "SERIALNUMBER"
  show (UnknownAttr x)  = show x

export
from_oid_attr : List Nat -> AttributeType
from_oid_attr oid =
  case map natToInteger oid of
    [ 2, 5, 4, 3 ]  => CommonName
    [ 2, 5, 4, 10 ] => Organization
    [ 2, 5, 4, 11 ] => OrganizationUnit
    [ 2, 5, 4, 6 ]  => Country
    [ 2, 5, 4, 8 ]  => StateOrProvince
    [ 2, 5, 4, 7 ]  => LocalityName
    [ 2, 5, 4, 5 ]  => SerialNumber
    _ => UnknownAttr oid

public export
record RelativeDistinguishedName where
  constructor MkRDN
  attributes : List (AttributeType, String)

public export
record DistinguishedName where
  constructor MkDN
  rdns : List RelativeDistinguishedName

public export
Eq RelativeDistinguishedName where
  a == b = (length a.attributes == length b.attributes) && ((a.attributes \\ b.attributes) == [])

public export
Eq DistinguishedName where
  a == b = a.rdns == b.rdns

export
dn_attributes : DistinguishedName -> List (AttributeType, String)
dn_attributes dn = dn.rdns >>= attributes

public export
Show DistinguishedName where
  show dn = join "," $ go <$> dn_attributes dn
    where
      go : (AttributeType, String) -> String
      go (attribute, content) = show attribute <+> "=" <+> content

extract_attr : ASN1Token -> Maybe (AttributeType, String)
extract_attr (Universal ** 16 ** Sequence [ (Universal ** 6 ** OID oid), string ]) = (from_oid_attr oid,) <$> extract_string string
extract_attr _ = Nothing

extract_rdn : ASN1Token -> Maybe RelativeDistinguishedName
extract_rdn (Universal ** 17 ** Set attributes) = MkRDN <$> traverse extract_attr attributes
extract_rdn _ = Nothing

extract_dn : ASN1Token -> Maybe DistinguishedName
extract_dn (Universal ** 16 ** Sequence rdns) = MkDN <$> traverse extract_rdn rdns
extract_dn _ = Nothing

public export
data ExtensionType : Type where
  BasicConstraint : ExtensionType
  KeyUsage : ExtensionType
  SubjectAltName : ExtensionType
  AuthorityKeyIdentifier : ExtensionType
  UnknownExt : List Nat -> ExtensionType

%runElab derive "ExtensionType" [Generic, Meta, Eq, DecEq, Show]

from_oid_ext : List Nat -> ExtensionType
from_oid_ext oid =
  case map natToInteger oid of
    [ 2, 5, 29, 15 ] => KeyUsage
    [ 2, 5, 29, 19 ] => BasicConstraint
    [ 2, 5, 29, 17 ] => SubjectAltName
    [ 2, 5, 29, 35 ] => AuthorityKeyIdentifier
    _ => UnknownExt oid

public export
record ExtBasicConstraint where
  constructor MkExtBasicConstraint
  ca : Bool
  path_len : Maybe Nat

public export
record ExtKeyUsage where
  constructor MkExtKeyUsage
  digital_signature : Bool
  non_repudiation   : Bool
  key_encipherment  : Bool
  data_encipherment : Bool
  key_agreement     : Bool
  key_cert_sign     : Bool
  crl_sign          : Bool
  encipher_only     : Bool
  decipher_only     : Bool

public export
data GeneralName : Type where
  DNSName : String -> GeneralName
  IPv4Addr : IPv4Addr -> GeneralName
  IPv6Addr : IPv6Addr -> GeneralName
  UnknownGN : ASN1Token -> GeneralName

public export
Show GeneralName where
  show (DNSName dns_name) = "DNS: " <+> dns_name
  show (IPv4Addr addr) = "IP Address: " <+> show addr
  show (IPv6Addr addr) = "IP Address: " <+> show addr
  show (UnknownGN _) = "<unknown>"

public export
Eq GeneralName where
  (DNSName a)  == (DNSName b) = a == b
  (IPv4Addr a) == (IPv4Addr b) = a == b
  (IPv6Addr a) == (IPv6Addr b) = a == b
  _ == _ = False

extract_general_name : ASN1Token -> Either String GeneralName
extract_general_name (ContextSpecific ** 2 ** UnknownPrimitive _ _ str) = Right $ DNSName $ ascii_to_string str
extract_general_name (ContextSpecific ** 7 ** UnknownPrimitive _ _ str) =
  let vec = fromList str
      gn = (IPv4Addr . MkIPv4Addr <$> exactLength 4 vec) <|> (IPv6Addr . MkIPv6Addr <$> exactLength 16 vec)
  in maybe_to_either gn "invalid IP address"
extract_general_name x = Right $ UnknownGN x

public export
record ExtSubjectAltName where
  constructor MkExtSubjectAltName
  general_names : List GeneralName

public export
record ExtAuthorityKeyIdentifier where
  constructor MkExtAuthorityKeyIdentifier
  key_identifier : Maybe (Vect 20 Bits8)
  general_names : List GeneralName
  serial_number : Maybe Integer

extract_auth_key_id : List ASN1Token -> Either String (List ASN1Token, Maybe (Vect 20 Bits8))
extract_auth_key_id [] = Right ([], Nothing)
extract_auth_key_id ((ContextSpecific ** 0 ** UnknownPrimitive _ _ key) :: xs) =
  (\c => (xs, Just c)) <$> (maybe_to_either (exactLength 20 $ fromList key) "invalid key id length")
extract_auth_key_id (x :: xs) = Right ((x :: xs), Nothing)

extract_auth_general_names : List ASN1Token -> Either String (List ASN1Token, List GeneralName)
extract_auth_general_names [] = Right ([], [])
extract_auth_general_names ((ContextSpecific ** 1 ** UnknownConstructed _ _ gns) :: xs) =
  (xs,) <$> traverse extract_general_name gns
extract_auth_general_names (x :: xs) = Right ((x :: xs), [])

extract_auth_serial_no : List ASN1Token -> Either String (Maybe Integer)
extract_auth_serial_no [] = Right Nothing
extract_auth_serial_no ((ContextSpecific ** 2 ** UnknownPrimitive _ _ serial_no) :: []) = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z serial_no) (parse_integer $ length serial_no)
  | (Pure leftover _) => Left $ "malformed serial number: leftover: " <+> (xxd $ map get leftover)
  | (Fail err) => Left $ show err
  | _ => Left "malformed serial number: underfed"
  pure $ Just ok
extract_auth_serial_no (x :: []) = Right Nothing
extract_auth_serial_no (x :: (y :: ys)) = Left "serial number is followed by unrecognized field"

public export
extension_type : ExtensionType -> Type
extension_type BasicConstraint = ExtBasicConstraint
extension_type KeyUsage = ExtKeyUsage
extension_type SubjectAltName = ExtSubjectAltName
extension_type AuthorityKeyIdentifier = ExtAuthorityKeyIdentifier
extension_type _ = List Bits8

parse_to_extension_type : (t : ExtensionType) -> List Bits8 -> Either String (extension_type t)
parse_to_extension_type BasicConstraint body = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1
  | (Pure leftover _) => Left $ "malformed basic constraint ext: leftover: " <+> (xxd $ map get leftover)
  | (Fail err) => Left $ show err
  | _ => Left "malformed basic constraint: underfed"
  let ( Universal ** 16 ** Sequence content ) = ok
  | _ => Left "malformed basic constraint: structure error"
  case content of
    [] =>
      Right (MkExtBasicConstraint False Nothing)
    [ (Universal ** 1 ** Boolean ca) ] =>
      Right (MkExtBasicConstraint ca Nothing)
    [ (Universal ** 1 ** Boolean ca), (Universal ** 2 ** IntVal depth) ] =>
      Right (MkExtBasicConstraint ca $ Just $ integerToNat depth)
    _ =>
      Left "malformed basic constraint: structure error"
parse_to_extension_type KeyUsage body = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1
  | (Pure leftover _) => Left $ "malformed key usage ext: leftover: " <+> (xxd $ map get leftover)
  | (Fail err) => Left $ show err
  | _ => Left "malformed key usage: underfed"
  let (Universal ** 3 ** Bitstring content) = ok
  | _ => Left "malformed key usage: structure error"
  case take 9 ((content.bytes >>= (toList . to_bools_be)) <+> replicate 9 False) of
    [a, b, c, d, e, f, g, h, i] => Right $ MkExtKeyUsage a b c d e f g h i
    _ => Left "impossible"
parse_to_extension_type SubjectAltName body = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1
  | (Pure leftover _) => Left $ "malformed subject alt name ext: leftover: " <+> (xxd $ map get leftover)
  | (Fail err) => Left $ show err
  | _ => Left "malformed subject alt name: underfed"
  let (Universal ** 16 ** Sequence content) = ok
  | _ => Left "malformed subject alt name: structure error"
  MkExtSubjectAltName <$> traverse extract_general_name content
parse_to_extension_type AuthorityKeyIdentifier body = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z body) parse_asn1
  | (Pure leftover _) => Left $ "malformed subject authority key id ext: leftover: " <+> (xxd $ map get leftover)
  | (Fail err) => Left $ show err
  | _ => Left "malformed subject authority key id: underfed"
  let (Universal ** 16 ** Sequence content) = ok
  | _ => Left "malformed subject authority key id: structure error"

  (content, key_id) <- extract_auth_key_id content
  (content, gns) <- extract_auth_general_names content
  sn <- extract_auth_serial_no content
  pure $ MkExtAuthorityKeyIdentifier key_id gns sn

parse_to_extension_type (UnknownExt x) body = Right body

public export
record Extension where
  constructor MkExt
  extension_id : ExtensionType
  critical : Bool
  value : extension_type extension_id

extract_extensions : List ASN1Token -> Either String (List Extension)
extract_extensions [] = Right []
extract_extensions (x :: xs) =
  case last (x :: xs) of
    (ContextSpecific ** 3 ** UnknownConstructed _ _ [ (Universal ** 16 ** Sequence extensions) ]) => traverse extract_ext extensions
    _ => Left "malformed extension list field"
  where
    extract_ext : ASN1Token -> Either String Extension
    extract_ext (Universal ** 16 ** Sequence
                [ (Universal ** 6 ** OID oid)
                , (Universal ** 1 ** Boolean critical)
                , (Universal ** 4 ** OctetString value)
                ]) = let ext_id = from_oid_ext oid in (MkExt ext_id critical) <$> parse_to_extension_type ext_id value
    extract_ext (Universal ** 16 ** Sequence
                [ (Universal ** 6 ** OID oid)
                , (Universal ** 4 ** OctetString value)
                ]) = let ext_id = from_oid_ext oid in (MkExt ext_id False) <$> parse_to_extension_type ext_id value
    extract_ext _ = Left "malformed extension field"

public export
record Certificate where
  constructor MkCertificate
  serial_number : Integer
  issuer : DistinguishedName
  valid_not_before : Integer
  valid_not_after : Integer
  subject : DistinguishedName
  cert_public_key : PublicKey
  cert_public_key_id : Vect 20 Bits8
  sig_parameter : SignatureParameter
  signature_value : BitArray
  extensions : List Extension
  tbs_raw_bytes : List Bits8

public export
Show Certificate where
  show cert = "Subject: " <+> show cert.subject <+> " Issuer: " <+> show cert.issuer

export
certificate_subject_names : Certificate -> List GeneralName
certificate_subject_names cert = go (toList (DNSName <$> common_name)) cert.extensions
  where
    go : List GeneralName -> List Extension -> List GeneralName
    go acc [] = acc
    go acc (x :: xs) =
      case x of
        MkExt SubjectAltName _ ext => go (acc <+> ext.general_names) xs
        _ => go acc xs
    common_name : Maybe String
    common_name = lookup CommonName $ dn_attributes cert.subject

export
is_self_signed : Certificate -> Bool
is_self_signed cert = cert.issuer == cert.subject

export
extract_extension : (type : ExtensionType) -> Certificate -> Maybe (extension_type type)
extract_extension type cert = go type cert.extensions
  where
    go : (type : ExtensionType) -> List Extension -> Maybe (extension_type type)
    go type (extension :: xs) =
      case decEq type extension.extension_id of
        Yes ok => Just $ rewrite ok in extension.value
        No _ => go type xs
    go type [] = Nothing

extract_tbs_raw_bytes : List Bits8 -> Either String (List Bits8)
extract_tbs_raw_bytes blob = do
  -- trim outer most layer
  let (Pure outer _) = feed (map (uncurry MkPosed) $ enumerate Z blob) (parse_tag_id *> parse_length)
  | (Fail err) => Left $ show err
  | _ => Left "malformed certificate: underfed"
  -- get the inner information
  let (Pure inner len) = feed outer (parse_tag_id *> parse_length)
  | (Fail err) => Left $ show err
  | _ => Left "malformed tbs certificate: underfed"

  let metadata = take (minus (length outer) (length inner)) outer
  pure (map get metadata <+> map get (take len inner))

export
parse_certificate : List Bits8 -> Either String Certificate
parse_certificate blob = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z blob) parse_asn1
  | (Pure leftover _) => Left $ "malformed certificate: leftover: " <+> (xxd $ map get leftover)
  | (Fail err) => Left $ show err
  | _ => Left "malformed certificate: underfed"

  let (Universal ** 16 ** Sequence
        [ (Universal ** 16 ** Sequence
          ( (ContextSpecific ** 0 ** UnknownConstructed _ _ [ (Universal ** 2 ** IntVal 2) ])
          :: (Universal ** 2 ** IntVal serial_number)
          :: crt_algorithm
          :: issuer
          :: (Universal ** 16 ** Sequence valid_period)
          :: subject
          :: certificate_public_key
          :: optional_fields
          ))
        , crt_signature_algorithm
        , (Universal ** 3 ** Bitstring signature_value)
        ]
      ) = ok
  | _ => Left "malformed certificate"

  let Just [ valid_not_before, valid_not_after ] = traverse {f=Maybe} extract_epoch valid_period
  | _ => Left "malformed validity timestamp"

  (key_id, key) <- extract_key' certificate_public_key

  crt_algorithm <- maybe_to_either (extract_algorithm crt_algorithm) "malformed certificate algorithm"
  crt_signature_algorithm <- maybe_to_either (extract_algorithm crt_signature_algorithm) "malformed certificate signature algorithm"

  let True = fst crt_algorithm == fst crt_signature_algorithm
  | False => Left "tbsCertificate signature field does not match signature algorithm"

  sig_param <- uncurry extract_signature_parameter crt_algorithm

  issuer <- maybe_to_either (extract_dn issuer) "malformed issuer"
  subject <- maybe_to_either (extract_dn subject) "malformed subject"

  extensions <- extract_extensions optional_fields

  raw_tbs_bytes <- extract_tbs_raw_bytes blob

  pure $
    MkCertificate
      serial_number
      issuer
      valid_not_before
      valid_not_after
      subject
      key
      key_id
      sig_param
      signature_value
      extensions
      raw_tbs_bytes


text:
module Test.Main

import Data.ByteString
import Data.List
import Data.SOP
import Data.Vect
import Hedgehog

--------------------------------------------------------------------------------
--          Generator
--------------------------------------------------------------------------------

smallBits32 : Gen Bits32
smallBits32 = bits32 (linear 0 10)

byte : Gen Bits8
byte = bits8 $ linear 0 0xff

byteList : Gen (List Bits8)
byteList = list (linear 0 30) byte

-- we make sure to not only generate `ByteString`s with
-- an offset of 0.
bytestring : Gen ByteString
bytestring =
  let bs1         = pack <$> byteList
      bs2         = [| substring smallBits32 smallBits32 bs1 |]
   in choice [bs1, bs2]

latinString : Gen String
latinString = string (linear 0 30) latin

--------------------------------------------------------------------------------
--          Properties
--------------------------------------------------------------------------------

unpackPack : Property
unpackPack = property $ do
  bs <- forAll byteList
  bs === unpack (pack bs)

packUnpack : Property
packUnpack = property $ do
  bs <- forAll bytestring
  bs === pack (unpack bs)

singletonHead : Property
singletonHead = property $ do
  b <- forAll byte
  Just b === head (singleton b)

packNull : Property
packNull = property $ do
  bs <- forAll byteList
  null bs === null (pack bs)

packLength : Property
packLength = property $ do
  bs <- forAll byteList
  length bs === cast (length $ pack bs)

consUncons : Property
consUncons = property $ do
  [b,bs] <- forAll $ np [byte,bytestring]
  Just (b,bs) === uncons (cons b bs)

unconsCons : Property
unconsCons = property $ do
  [b,bs] <- forAll $ np [byte,bytestring]
  let bs' = cons b bs
  Just bs' === map (uncurry cons) (uncons bs')

snocUnsnoc : Property
snocUnsnoc = property $ do
  [b,bs] <- forAll $ np [byte,bytestring]
  Just (b,bs) === unsnoc (snoc b bs)

unsnocSnoc : Property
unsnocSnoc = property $ do
  [b,bs] <- forAll $ np [byte,bytestring]
  let bs' = snoc b bs
  Just bs' === map (uncurry snoc) (unsnoc bs')

appendNeutralLeft : Property
appendNeutralLeft = property $ do
  bs <- forAll bytestring
  bs === (neutral <+> bs)

appendNeutralRight : Property
appendNeutralRight = property $ do
  bs <- forAll bytestring
  bs === (bs <+> neutral)

appendAssociative : Property
appendAssociative = property $ do
  [bs1,bs2,bs3] <- forAll $ np [bytestring,bytestring,bytestring]
  ((bs1 <+> bs2) <+> bs3) === (bs1 <+> (bs2 <+> bs3))

prop_fastConcat : Property
prop_fastConcat = property $ do
  bss <- forAll (list (linear 0 10) byteList)
  fastConcat (pack <$> bss) === pack (concat bss)

consHead : Property
consHead = property $ do
  [b,bs] <- forAll $ np [byte, bytestring]
  Just b === head (cons b bs)

snocLast : Property
snocLast = property $ do
  [b,bs] <- forAll $ np [byte, bytestring]
  Just b === last (snoc b bs)

consTail : Property
consTail = property $ do
  [b,bs] <- forAll $ np [byte, bytestring]
  Just bs === tail (cons b bs)

snocInit : Property
snocInit = property $ do
  [b,bs] <- forAll $ np [byte, bytestring]
  Just bs === init (snoc b bs)

prop_substring : Property
prop_substring = property $ do
  [start,len,str] <- forAll $ np [smallBits32,smallBits32,latinString]
  let ss = substring start len (fromString str)

  fromString (substr (cast start) (cast len) str) ===
  substring start len (fromString str)

reverseReverse : Property
reverseReverse = property $ do
  bs <- forAll bytestring
  bs === reverse (reverse bs)

fun : Bits8 -> Maybe Bits8
fun b = if b < 128 then Just (128 - b) else Nothing

prop_mapMaybe : Property
prop_mapMaybe = property $ do
  bs <- forAll byteList
  mapMaybe fun (pack bs) === pack (mapMaybe fun bs)

prop_filter : Property
prop_filter = property $ do
  bs <- forAll byteList
  filter (< 100) (pack bs) === pack (filter (< 100) bs)

prop_take : Property
prop_take = property $ do
  [n,bs] <- forAll $ np [nat (linear 0 30), byteList]
  take (cast n) (pack bs) === pack (take n bs)

prop_takeEnd : Property
prop_takeEnd = property $ do
  [n,bs] <- forAll $ np [bits32 (linear 0 30), bytestring]
  takeEnd n bs === reverse (take n $ reverse bs)

prop_drop : Property
prop_drop = property $ do
  [n,bs] <- forAll $ np [nat (linear 0 30), byteList]
  drop (cast n) (pack bs) === pack (drop n bs)

prop_dropEnd : Property
prop_dropEnd = property $ do
  [n,bs] <- forAll $ np [bits32 (linear 0 30), bytestring]
  dropEnd n bs === reverse (drop n $ reverse bs)

prop_takeWhile : Property
prop_takeWhile = property $ do
  bs <- forAll byteList
  takeWhile (< 100) (pack bs) ===
  pack (takeWhile (< 100) bs)

prop_takeWhileEnd : Property
prop_takeWhileEnd = property $ do
  bs <- forAll bytestring
  takeWhileEnd (< 100) bs ===
  reverse (takeWhile (< 100) $ reverse bs)

prop_dropWhileEnd : Property
prop_dropWhileEnd = property $ do
  bs <- forAll bytestring
  dropWhileEnd (< 100) bs ===
  reverse (dropWhile (< 100) $ reverse bs)

prop_breakAppend : Property
prop_breakAppend = property $ do
  bs <- forAll bytestring
  let (a,b) = break (< 100) bs
  bs === (a <+> b)

prop_breakFirst : Property
prop_breakFirst = property $ do
  bs <- forAll bytestring
  let (a,b) = break (< 100) bs
  assert $ all (>= 100) a

main : IO ()
main = test . pure $ MkGroup "ByteString"
  [ ("unpackPack", unpackPack)
  , ("packUnpack", packUnpack)
  , ("consUncons", consUncons)
  , ("unsnocSnoc", unsnocSnoc)
  , ("snocUnsnoc", snocUnsnoc)
  , ("unconsCons", unconsCons)
  , ("singletonHead", singletonHead)
  , ("packNull", packNull)
  , ("packLength", packLength)
  , ("appendNeutralRight", appendNeutralRight)
  , ("appendNeutralLeft", appendNeutralLeft)
  , ("appendAssociative", appendAssociative)
  , ("prop_fastConcat", prop_fastConcat)
  , ("consHead", consHead)
  , ("consTail", consTail)
  , ("snocLast", snocLast)
  , ("snocInit", snocInit)
  , ("prop_substring", prop_substring)
  , ("reverseReverse", reverseReverse)
  , ("prop_mapMaybe", prop_mapMaybe)
  , ("prop_filter", prop_filter)
  , ("prop_drop", prop_drop)
  , ("prop_take", prop_take)
  , ("prop_takeWhile", prop_takeWhile)
  , ("prop_takeWhileEnd", prop_takeWhileEnd)
  , ("prop_dropWhileEnd", prop_dropWhileEnd)
  , ("prop_breakAppend", prop_breakAppend)
  , ("prop_breakFirst", prop_breakFirst)
  ]


text:
module Main

import Pretty

main : IO ()
main = putStrLn "huzzah!"


text:
module Data.Path

%default total

||| Paths in a typed graph as a sequence of edges with source and target nodes matching up domino-style.
||| AKA reflexive-transitive closure.
public export
data Path : (t -> t -> Type) -> t -> t -> Type where
  Nil  : Path g i i
  (::) : {0 i, j, k : t} ->
         g i j -> Path g j k -> Path g i k

export
joinPath : Path g i j -> Path g j k -> Path g i k
joinPath []      jk = jk
joinPath (e::ij) jk = e :: joinPath ij jk

export
snocPath : Path g i j -> g j k -> Path g i k
snocPath []      f = [f]
snocPath (e::ij) f = e :: snocPath ij f

export
lengthPath : Path g i j -> Nat
lengthPath []     = Z
lengthPath (_::p) = S $ lengthPath p

export
mapPath : {0 gt : t -> t -> Type} -> {0 gu : u -> u -> Type} -> {0 f : t -> u}
       -> ({0 i, j : t} ->      gt i j ->      gu (f i) (f j))
       ->  {0 i, j : t} -> Path gt i j -> Path gu (f i) (f j)
mapPath gf []     = []
mapPath gf (e::p) = gf e :: mapPath gf p

export
foldPath : {0 gt : t -> t -> Type} -> {0 gu : u -> u -> Type} -> {0 f : t -> u}
        -> ({0 i, j, k : t} ->      gt i j -> gu (f j) (f k) -> gu (f i) (f k))
        ->  {0 i, j, k : t} -> Path gt i j -> gu (f j) (f k) -> gu (f i) (f k)
foldPath gf []      jk = jk
foldPath gf (e::ij) jk = gf e (foldPath {gu} gf ij jk)

export
foldlPath : {0 gt : t -> t -> Type} -> {0 gu : u -> u -> Type} -> {0 f : t -> u}
        -> ({0 i, j, k : t} -> gu (f i) (f j) ->      gt j k -> gu (f i) (f k))
        ->  {0 i, j, k : t} -> gu (f i) (f j) -> Path gt j k -> gu (f i) (f k)
foldlPath gf ij []      = ij
foldlPath gf ij (e::jk) = foldlPath {gu} gf (gf ij e) jk


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

module Toolkit.Options.ArgParse.Error

import Data.String

import System.File

import Toolkit.Data.Location

import Toolkit.Options.ArgParse.Model
import Toolkit.Options.ArgParse.Lexer
import Toolkit.Options.ArgParse.Parser

%default total

public export
data ArgParseError : Type where
  InvalidOption   : Arg -> ArgParseError
  MalformedOption : ParseError Token -> ArgParseError

export
(Show Arg) => Show ArgParseError where
  show (InvalidOption o) = "Invalid Option " ++ show o
  show (MalformedOption (PError (MkParseFail error location rest))) =
    unlines [show location, error]
  show (MalformedOption (LError (MkLexFail l i)))  = unwords [show l, ":\n" <+> i]
  show (MalformedOption (FError x))  = unlines ["File Error:", show x]

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module System.File.Handle

import public System.File.Error
import public System.File.Mode
import System.File.Support
import public System.File.Types
import System.FFI

%default total

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign support "idris2_openFile"
         "node:support:openFile,support_system_file"
         jvm' fileClass "open" "String String" fileClass
prim__open : String -> String -> PrimIO FilePtr

%foreign support "idris2_closeFile"
         "node:lambda:(fp) => require('fs').closeSync(fp.fd)"
         jvm' fileClass "close" fileClass "void"
prim__close : FilePtr -> PrimIO ()

export
openFile : HasIO io => String -> Mode -> io (Either FileError File)
openFile f m
    = do res <- primIO (prim__open f (modeStr m))
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (FHandle res)

export
closeFile : HasIO io => File -> io ()
closeFile (FHandle f) = primIO (prim__close f)

||| Perform a given operation on successful file open
||| and ensure the file is closed afterwards or perform
||| a different operation if the file fails to open.
export
withFile : HasIO io => (filename : String) ->
                       Mode ->
                       (onError : FileError -> io a) ->
                       (onOpen  : File -> io (Either a b)) ->
                       io (Either a b)
withFile filename mode onError onOpen =
  do Right h <- openFile filename mode
       | Left err => Left <$> onError err
     res <- onOpen h
     closeFile h
     pure res


text:
module Main

import Coda.Node.Core
import Coda.Node.HTTP
import Coda.Node.FS

%default total

{-
  HTTP Helpers
-}

queryParams : Ptr -> JS_IO (List String)
queryParams req = Strings.split (== '?') <$> prop { ty = String } req "url"

end : Ptr -> String -> JS_IO ()
end res = method { a = String } { b = () } res "end"

{-
  Route Handlers
-}

handleIndex : Ptr -> Ptr -> JS_IO ()
handleIndex req res = do
  fs <- require "fs"
  indexFile <- readFileSync fs "./index.html"
  end res indexFile

handleRun : Ptr -> Ptr -> JS_IO ()
handleRun req res = do
  [_, query] <- queryParams req | _ => end res "Needs a query"
  log query
  end res query

handle404 : Ptr -> Ptr -> JS_IO ()
handle404 _ res = end res "Invalid route"

route : (String, String) -> Ptr -> Ptr -> JS_IO ()
route ("GET", "/")    = handleIndex
route ("GET", "/run") = handleRun
route _ = handle404

partial
router : HTTP.Handler
router req res = do
  verb <- prop { ty = String } req "method"
  [path, query] <- queryParams req
  log (verb ++ " " ++ path ++ " ? " ++ query)
  route (verb, path) req res

partial
main : JS_IO ()
main = do server <- createServer router
          listen server (MkPort 2112)

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
module Tools.Indexed

%access public export

interface IxFunctor (idx : Type) (f : idx -> Type -> Type) where
  imap : {i : idx} -> (a -> b) -> f i a -> f i b

interface IxFunctor idx f => IxPointed idx (f : idx -> Type -> Type) where
  ireturn : {i : idx} -> a -> f i a

interface IxFunctor idx f => IxCopointed idx (f : idx -> Type -> Type) where
  iextract : {i : idx} -> f i a -> a

interface IxPointed idx f => IxApplicative idx (f : idx -> Type -> Type) where
  iapp : {i : idx} -> f i (a -> b) -> f i a -> f i b

interface IxFoldable (idx : Type) (f : idx -> Type -> Type) where
  ifoldMap : Monoid m => {i : idx} -> (a -> m) -> f i a -> m


text:
module SmallStepCombined

%access public export

%default total

data Tm : Type where
  C : Nat -> Tm
  P : Tm -> Tm -> Tm
  Tru : Tm
  Fls : Tm
  If : Tm -> Tm -> Tm -> Tm

data Value : Tm -> Type where
  V_Const : (n : Nat) -> Value (C n)
  V_Tru : Value Tru
  V_Fls : Value Fls

Uninhabited (Value (P _ _)) where
  uninhabited (V_Const _) impossible
  uninhabited V_Tru impossible
  uninhabited V_Fls impossible

data Step : Tm -> Tm -> Type where
  ST_PlusConstConst : Step (P (C n1) (C n2)) (C (n1 + n2))
  ST_Plus1 : Step t1 t1' -> Step (P t1 t2) (P t1' t2)
  ST_Plus2 : Value v1 -> Step t2 t2' -> Step (P v1 t2) (P v1 t2')
  ST_IfTrue : Step (If Tru t1 t2) t1
  ST_IfFalse : Step (If Fls t1 t2) t2
  ST_If : Step t1 t1' -> Step (If t1 t2 t3) (If t1' t2 t3)

Uninhabited (Step (C n) _) where
  uninhabited ST_PlusConstConst impossible
  uninhabited (ST_Plus1 _) impossible
  uninhabited (ST_Plus2 _ _) impossible
  uninhabited ST_IfTrue impossible
  uninhabited ST_IfFalse impossible
  uninhabited (ST_If _) impossible

Uninhabited (Step Tru _) where
  uninhabited ST_PlusConstConst impossible
  uninhabited (ST_Plus1 _) impossible
  uninhabited (ST_Plus2 _ _) impossible
  uninhabited ST_IfTrue impossible
  uninhabited ST_IfFalse impossible
  uninhabited (ST_If _) impossible

Uninhabited (Step Fls _) where
  uninhabited ST_PlusConstConst impossible
  uninhabited (ST_Plus1 _) impossible
  uninhabited (ST_Plus2 _ _) impossible
  uninhabited ST_IfTrue impossible
  uninhabited ST_IfFalse impossible
  uninhabited (ST_If _) impossible

infix 4 -+>

(-+>) : Tm -> Tm -> Type
(-+>) = Step

step_deterministic : Step x y1 -> Step x y2 -> y1 = y2
step_deterministic ST_PlusConstConst ST_PlusConstConst = Refl
step_deterministic (ST_Plus1 s1) (ST_Plus2 (V_Const _) _) = absurd s1
step_deterministic (ST_Plus1 s1) (ST_Plus2 V_Tru _) = absurd s1
step_deterministic (ST_Plus1 s1) (ST_Plus2 V_Fls _) = absurd s1
step_deterministic (ST_Plus2 (V_Const _) _) (ST_Plus1 s1) = absurd s1
step_deterministic (ST_Plus2 V_Tru _) (ST_Plus1 s1) = absurd s1
step_deterministic (ST_Plus2 V_Fls _) (ST_Plus1 s1) = absurd s1
step_deterministic (ST_Plus1 s1) (ST_Plus1 s2) =
  rewrite step_deterministic s1 s2
  in Refl
step_deterministic (ST_Plus2 v1 s1) (ST_Plus2 v2 s2) =
  rewrite step_deterministic s1 s2
  in Refl
step_deterministic ST_IfTrue ST_IfTrue = Refl
step_deterministic ST_IfFalse ST_IfFalse = Refl
step_deterministic (ST_If s1) (ST_If s2) =
  rewrite step_deterministic s1 s2
  in Refl

strong_progress : (t : Tm ** (Not (Value t), Not (t' : Tm ** t -+> t')))
strong_progress = (P Tru (C 0) ** ( \v => absurd v
                                  , \(_ ** s) => case s of
                                      ST_Plus1 s1 => absurd s1
                                      ST_Plus2 _ s2 => absurd s2 ))


text:
module Algebra.ZeroOneOmega

import Algebra.Semiring
import Algebra.Preorder

%default total

export
data ZeroOneOmega = Rig0 | Rig1 | RigW

export
Preorder ZeroOneOmega where
  Rig0 <= _ = True
  Rig1 <= Rig1 = True
  Rig1 <= RigW = True
  RigW <= RigW = True
  _ <= _ = False
  preorderRefl {x = Rig0} = Refl
  preorderRefl {x = Rig1} = Refl
  preorderRefl {x = RigW} = Refl
  preorderTrans {x = Rig0} {y = y} {z = z} a b = Refl
  preorderTrans {x = Rig1} {y = Rig0} {z = Rig0} Refl Refl impossible
  preorderTrans {x = Rig1} {y = Rig1} {z = Rig0} _ Refl impossible
  preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ Refl impossible
  preorderTrans {x = Rig1} {y = y} {z = Rig1} a b = Refl
  preorderTrans {x = Rig1} {y = y} {z = RigW} a b = Refl
  preorderTrans {x = RigW} {y = Rig0} {z = _} Refl _ impossible
  preorderTrans {x = RigW} {y = Rig1} {z = _} Refl _ impossible
  preorderTrans {x = RigW} {y = RigW} {z = z} a b = b

public export
Eq ZeroOneOmega where
  (==) Rig0 Rig0 = True
  (==) Rig1 Rig1 = True
  (==) RigW RigW = True
  (==) _ _ = False

export
Show ZeroOneOmega where
  show Rig0 = "Rig0"
  show Rig1 = "Rig1"
  show RigW = "RigW"

export
rigPlus : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
rigPlus Rig0 a = a
rigPlus a Rig0 = a
rigPlus Rig1 a = RigW
rigPlus a Rig1 = RigW
rigPlus RigW RigW = RigW

export
rigMult : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
rigMult Rig0 _ = Rig0
rigMult _ Rig0 = Rig0
rigMult Rig1 a = a
rigMult a Rig1 = a
rigMult RigW RigW = RigW

public export
Semiring ZeroOneOmega where
  (|+|) = rigPlus
  (|*|) = rigMult
  plusNeutral = Rig0
  timesNeutral = Rig1

||| The top value of a lattice
export
Top ZeroOneOmega where
  top = RigW
  topAbs {x = Rig0} = Refl
  topAbs {x = Rig1} = Refl
  topAbs {x = RigW} = Refl


text:
init : a -> c -> List b -> List (a, b, c)
init a c = map (uncurry (,)) . map (a,) . map (,c)

unzip : List (a, b) -> (List a, List b)
unzip [] = ([], [])
unzip ((a, b) :: abs)
  = let (as, bs) = unzip abs in
    (a :: as, b :: bs)

unzip4 : List (a, b, c, d) -> (List a, List b, List c, List d)
unzip4 [] = ([], [], [], [])
unzip4 (abcd :: abcds)
  = let (a, b, c, d) = abcd
        (as, bs, cs, ds) = unzip4 abcds
    in (a :: as, b :: bs, c :: cs, d :: ds)


text:
import Aoc
import Data.Fin
import Data.List
import Data.Nat
import Data.Stream
import Data.Vect
%default total

data Square = Tree | Open

isTree : Square -> Bool
isTree Tree = True
isTree _ = False

||| Parse a character of input as a grid square.
parseSquare : Char -> Maybe Square
parseSquare '#' = Just Tree
parseSquare '.' = Just Open
parseSquare _ = Nothing

||| A grid of n rows, each having (m'+1) squares.
Grid : (n : Nat) -> (m' : Nat) -> Type
Grid n m' = Vect n (Vect (S m') Square)

data ParseError = UnrecognizedChar | NotRectangular | WidthZero
Show ParseError where
  show UnrecognizedChar = "unrecognized char"
  show NotRectangular = "not rectangular"
  show WidthZero = "width is zero"

||| Parse the input grid (given as a list of lines).
parseGrid : List String -> Either ParseError (n : Nat ** m' : Nat ** Grid n m')
parseGrid ls =
  case traverse (traverse parseSquare . unpack) ls of
    Nothing => Left UnrecognizedChar
    Just rs =>
      let n = length ls
          m = case ls of l::_ => length l; _ => Z
      in case toMatrix n m rs of
        Nothing => Left NotRectangular
        Just mat =>
          case m of
            Z => Left WidthZero
            S m' => Right (n ** (m' ** mat))

||| Get elements 0, k+1, 2(k+1), ... of a list.
||| (That is: yield an element, skip k elements, repeat.)
gaps : Nat -> List a -> List a
gaps k xs = go Z xs
  where go : Nat -> List a -> List a
        go _ [] = []
        go Z (x::xs) = x :: go k xs
        go (S i) (x::xs) = go i xs

||| Get all squares we run into on the slope (right, down) in the grid.
||| "down" must be provably positive: otherwise we'd never reach the bottom.
traceSlope : {m' : Nat} -> (right : Nat) -> (down : Nat) -> {auto _ : IsSucc down} -> Grid n m' -> List Square
traceSlope right down@(S d') grid =
  let rows = gaps d' (toList grid)
  in drop 1 $ go Z rows
  where go : Nat -> List (Vect (S m') Square) -> List Square
        go i (r::rs) = mindex i r :: go (i + right) rs
        go i [] = []

||| Get the "score" (number of trees) for a slope.
score : {m' : Nat} -> (right : Nat) -> (down : Nat) -> {auto _ : IsSucc down} -> Grid n m' -> Nat
score right down grid =
  count isTree (traceSlope right down grid)

partial
main : IO ()
main = do
  ls <- readLines
  case parseGrid ls of
    Left error => printLn error
    Right (n ** (m' ** grid)) => do
      putStr "*   "
      printLn $ score 3 1 grid
      putStr "**  "
      let slopes : List (Nat, Nat) = [(1,1),(3,1),(5,1),(7,1),(1,2)]
      printLn $ product [score r d grid | (r,d@(S _)) <- slopes]


text:
module Main

import GLCore
import JSArrays
import Shaders

import JSMatrix.JSMatrix

-- Save time, just get the canvas directly by id
getElemById : String -> IO Element
getElemById s = do
  x <- mkForeign (FFun "document.getElementById(%0)" [FString] FPtr) s
  return (MkElem x)

getElemFloatProp : String -> Element -> IO Float
getElemFloatProp p (MkElem e) = mkForeign (FFun "%0[%1]" [FPtr,FString] FFloat) e p

getElemStringProp : String -> Element -> IO String
getElemStringProp p (MkElem e) = mkForeign (FFun "%0[%1]" [FPtr,FString] FString) e p

-- Retrieve the dimensions of the canvas element
canvasDimensions : Element -> IO (List Float)
canvasDimensions e = do
  w <- getElemFloatProp "width" e
  h <- getElemFloatProp "height" e
  return [w,h]

-- Shader Functions
getShader : String -> IO String
getShader e = getElemById e >>= getElemStringProp "textContent"

-- Pyramid
pyramidVertices : List Float
pyramidVertices = [0.0, 1.0, 0.0,
                   -1.0, 0.0, 1.0,
                   1.0, 0.0, 1.0,

                   0.0, 1.0, 0.0,
                   1.0, 0.0, 1.0,
                   1.0, 0.0, -1.0,

                   0.0, 1.0, 0.0,
                   1.0, 0.0, -1.0,
                   -1.0, 0.0, -1.0,

                   0.0, 1.0, 0.0,
                   -1.0, 0.0, -1.0,
                   -1.0, 0.0, 1.0]

pyramidColours : List Float
pyramidColours = [0, 0, 1, 1,
                  0, 0, 1, 1,
                  0, 0, 1, 1,

                  1, 1, 0, 1,
                  1, 1, 0, 1,
                  1, 1, 0, 1,

                  0, 1, 0, 1,
                  0, 1, 0, 1,
                  0, 1, 0, 1,

                  1, 0, 0, 1,
                  1, 0, 0, 1,
                  1, 0, 0, 1]

mvTranslateVect : Vect 3 Float
mvTranslateVect = [0.0,0.0,-4.0]

rotateVec : Vect 3 Float
rotateVec = [0.0,1.0,0.0]

-- Some basic settings for starting our GL env
baseGLInit : GLCxt -> IO GLCxt
baseGLInit c = do
  depthTest <- getGLProp "DEPTH_TEST" c
  clearColor [1.0, 1.0, 1.0, 1.0] c >>= enableGLSetting depthTest >>= glClear

prepareVerticesArray : List Float -> IO F32Array
prepareVerticesArray xs = createJSArray >>= fromFloatList xs >>= createF32Array

-- Wrapper for finding and init'ing our GL env and context
locateInitCanvas : IO GLCxt
locateInitCanvas = getElemById "canvas" >>= getGLCxt >>= baseGLInit

-- Wrapper for the process of assigning a shader variable the correct location
-- for our program to locate vertex information when the shader runs.
assignVertexPositionAttribs : String -> Int -> (GLProgram,GLCxt) -> IO (GLProgram,GLCxt)
assignVertexPositionAttribs attr n glProg = do
  loc <- getAttribLocation attr glProg
  enableVertexAttribArray glProg loc >>= setVertexAttribPointer n loc

translateMat : JSGLMat4 -> IO JSGLMat4
translateMat jsMat4 =
  createVec3FromVect mvTranslateVect >>= \v3 => translateM4 v3 jsMat4 jsMat4

printJunk : JSGLMat4 -> IO ()
printJunk (MkMat4 a) = mkForeign (FFun "console.log(%0)" [FPtr] FUnit) a

main : IO ()
main = do
  [w,h] <- getElemById "canvas" >>= canvasDimensions
  verticesF32 <- prepareVerticesArray pyramidVertices
  coloursF32 <- prepareVerticesArray pyramidColours

  (vBuffer,glCxt) <- locateInitCanvas >>= flip createBindBuffer verticesF32
  (cBuffer,glCxt') <- createBindBuffer glCxt coloursF32

  -- Set the viewport size
  setViewport w h glCxt'

  prgCxt <- createProg glCxt'

  -- Pull the shaders off the DOM
  vshader <- [| Vertex $ getShader "vshader" |]
  fshader <- [| Fragment $ getShader "fshader" |]

  -- JS Math.Pi Value
  mPI <- mathPI

  -- Create rotation vector
  rotationAxis <- createVec3
  rotationAxis' <- createVec3FromVect rotateVec >>= normaliseV3 rotationAxis

  -- Create our matrices
  mvMatrix <- createMat4 >>= translateMat
  mvMatrix' <- rotateM4 mvMatrix (mPI*2*33) rotationAxis' mvMatrix

  pjMatrix <- createMat4 >>= perspectiveM4 (mPI/4) (w/h) 1 100

  -- Pass our shader code to be built,compiled, and linked to the GL context
  prgCxt' <- compileAndLinkShaders [vshader, fshader] prgCxt >>= useProg

  prgCxt'' <- assignVertexPositionAttribs "vertPos" 3 prgCxt'
  nxtPrgCxt <- assignVertexPositionAttribs "vertColor" 4 prgCxt''

  mvLoc <- getUniformLocation "mvMatrix" nxtPrgCxt
  pjLoc <- getUniformLocation "pjMatrix" nxtPrgCxt

  nxtPrgCxt' <- uniformMatrix4v mvMatrix' mvLoc nxtPrgCxt >>= uniformMatrix4v pjMatrix pjLoc

  drawTriangles 0 12 nxtPrgCxt'

  putStrLn "It might have worked... who knows!"

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module HelloWorld

export
hello : String
hello = ?hello_rhs

export
version : String
version = "1.0.0"

max_stars_repo_name: exercism-bot/idris

max_issues_repo_name: exercism-bot/idris

max_forks_repo_name: exercism-bot/idris


text:
module TTImp.Interactive.MakeLemma

import Core.Context
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.TT
import Core.Value

import TTImp.Unelab
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Utils

import Data.List

%default covering

used : RigCount -> Bool
used = not . isErased

hiddenName : Name -> Bool
hiddenName (MN "_" _) = True
hiddenName _ = False

-- True if the variable appears guarded by a constructor in the term
bindable : Nat -> Term vars -> Bool
bindable p tm
    = case getFnArgs tm of
           (Ref _ (TyCon _ _) n, args) => any (bindable p) args
           (Ref _ (DataCon _ _) _, args) => any (bindable p) args
           (TDelayed _ _ t, args) => any (bindable p) (t :: args)
           (TDelay _ _ _ t, args) => any (bindable p) (t :: args)
           (TForce _ _ t, args) => any (bindable p) (t :: args)
           (Local _ _ p' _, []) => p == p'
           _ => False

bindableArg : Nat -> Term vars -> Bool
bindableArg p (Bind _ _ (Pi _ _ _ ty) sc)
   = bindable p ty || bindableArg (1 + p) sc
bindableArg p _ = False

getArgs : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          Env Term vars -> Nat -> Term vars ->
          Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp)
getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc)
    = do defs <- get Ctxt
         ty' <- map (map rawName) $ unelab env !(normalise defs env ty)
         let x' = UN $ Basic !(uniqueName defs (map nameRoot vars) (nameRoot x))
         (sc', ty) <- getArgs (b :: env) k (renameTop x' sc)
         -- Don't need to use the name if it's not used in the scope type
         let mn = if c == top
                       then case shrinkTerm sc (DropCons SubRefl) of
                                    Nothing => Just x'
                                    _ => Nothing
                       else Just x'
         let p' = if used c && not (bindableArg 0 sc) && not (hiddenName x)
                     then Explicit
                     else Implicit
         pure ((x, mn, p', c, ty') :: sc', ty)
getArgs env k ty
      = do defs <- get Ctxt
           ty' <- map (map rawName) $ unelab env !(normalise defs env ty)
           pure ([], ty')

mkType : FC -> List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) ->
         RawImp -> RawImp
mkType loc [] ret = ret
mkType loc ((_, n, p, c, ty) :: rest) ret
    = IPi loc c p n ty (mkType loc rest ret)

mkApp : FC -> Name ->
        List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) -> RawImp
mkApp loc n args
    = apply (IVar loc n) (mapMaybe getArg args)
  where
    getArg : (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) ->
             Maybe RawImp
    getArg (x, _, Explicit, _, _) = Just (IVar loc x)
    getArg _ = Nothing

-- Return a top level type for the lemma, and an expression which applies
-- the lemma to solve a hole with 'locs' arguments
export
makeLemma : {auto m : Ref MD Metadata} ->
            {auto c : Ref Ctxt Defs} ->
            FC -> Name -> Nat -> ClosedTerm ->
            Core (RawImp, RawImp)
makeLemma loc n nlocs ty
    = do defs <- get Ctxt
         (args, ret) <- getArgs [] nlocs !(normalise defs [] ty)
         pure (mkType loc args ret, mkApp loc n args)


text:
import Data.Vect

%default total

-- variable
x : Int
x = 5

-- function1 incr
incr : Int -> Int
incr x = x + 1

-- function2 add
add : Int -> Int -> Int
add x y = x + y

-- adt sum type
data TrafficLight = Red | Yellow | Green

-- function adt show
show : TrafficLight -> String
show Red = "R"
show Yellow = "Y"
show Green = "G"

-- mylist
data MyList : Type -> Type where
  Empty : MyList t
  Cons : (elem : t) -> MyList t -> MyList t

-- variable xs vect
xs : Vect 3 Int
xs = [1,2,3]

-- vtake
vtake : (n:Nat) -> Vect (n+m) t -> Vect n t
vtake Z xs = []
vtake (S k) (x :: xs) = x :: vtake k xs

-- vtake to string
elems : String
elems = show ( vtake 2 [1,2,3,4] )

-- vappend
vappend : Vect n t -> Vect m t -> Vect (n+m) t
vappend [] ys = ys
vappend (x :: xs) ys = x :: vappend xs ys


text:
module ColistFun

-- Inspired by a pull request https://github.com/idris-lang/Idris2/pull/997
-- by Stefan Hoeck and by discussion started by Mathew Polzin.

data Colist : Type -> Type where
  Nil  : Colist a
  (::) : a -> Inf (Colist a) -> Colist a

Functor Colist where
  map f []      = []
  map f (x::xs) = f x :: map f xs

functorId : (xs : Colist a) -> map Prelude.id xs = xs
functorId [] = Refl
functorId (x::Delay xs) = cong (x::) $ functorId xs


text:
module Language.JSON.String.Tokens

import Data.String.Extra
import Text.Token

%default total

public export
data JSONStringTokenKind
  = JSTQuote
  | JSTChar
  | JSTSimpleEscape
  | JSTUnicodeEscape

public export
JSONStringToken : Type
JSONStringToken = Token JSONStringTokenKind

public export
Eq JSONStringTokenKind where
  (==) JSTQuote JSTQuote = True
  (==) JSTChar JSTChar = True
  (==) JSTSimpleEscape JSTSimpleEscape = True
  (==) JSTUnicodeEscape JSTUnicodeEscape = True
  (==) _ _ = False

private
charValue : String -> Char
charValue x = case index 0 x of
                   Nothing => '\NUL'
                   Just c  => c

private
simpleEscapeValue : String -> Char
simpleEscapeValue x
  = case index 1 x of
         Nothing => '\NUL'
         Just c => case c of
                        '"'  => '"'
                        '\\' => '\\'
                        '/'  => '/'
                        'b'  => '\b'
                        'f'  => '\f'
                        'n'  => '\n'
                        'r'  => '\r'
                        't'  => '\t'
                        _    => '\NUL'

private
unicodeEscapeValue : String -> Char
unicodeEscapeValue x = chr $ cast ("0x" ++ drop 2 x)

public export
TokenKind JSONStringTokenKind where
  TokType JSTQuote = ()
  TokType JSTChar = Char
  TokType JSTSimpleEscape = Char
  TokType JSTUnicodeEscape = Char

  tokValue JSTQuote = const ()
  tokValue JSTChar = charValue
  tokValue JSTSimpleEscape = simpleEscapeValue
  tokValue JSTUnicodeEscape = unicodeEscapeValue


text:
module Deps.Parser

-- Implementation heavily inspired by Idris' Language.JSON and Blodwen

import public Text.Parser

import Deps.Data
import Deps.Lexer

%default total
%access public export

Parser : Type -> Type
Parser a = Grammar IdrisToken True a

symbol : String -> Parser ()
symbol expectedName = do
  symbolName <- match Symbol
  if symbolName == expectedName
    then pure ()
    else fail ("Expected: " ++ expectedName)

exactIdent : String -> Parser ()
exactIdent expectedName = do
  identName <- match Identifier
  if identName == expectedName
    then pure ()
    else fail ("Expected: " ++ expectedName)

namespace_ : Parser Namespace
namespace_ = do
  ns <- sepBy1 (symbol ".") (match Identifier)
  pure ns

module_ : Parser Namespace
module_ = do
  exactIdent "module"
  namespace_

import_ : Parser Import
import_ = do
  exactIdent "import"
  reexp <- option False (do
    exactIdent "public"
    pure True)
  ns <- namespace_
  nsAs <- option ns (do
    exactIdent "as"
    namespace_)
  pure (MkImport reexp ns nsAs)

program : Grammar IdrisToken False IdrisHead
program = do
  moduleNs <- option defaultModuleNs module_
  imports <- many import_
  pure (MkIdrisHead moduleNs imports)

runParser : String -> Grammar IdrisToken e a -> Maybe a
runParser str parser =
  let
    tokens = map tok (runLexer str)
    validTokens = filter (not . ignored) tokens
    Right (res, _) = parse parser validTokens
      | Nothing
  in Just res

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module Cordial.Model.Common.Whole

%default total
%access public export

data Whole : Type where
  W : (n : Nat) -> (prf : IsSucc n) -> Whole

data IsOne : Whole -> Type where
  ItIsOne : IsOne (W (S Z) ItIsSucc)

wholeIsNotOne : Not (IsOne $ W (S (S n)) ItIsSucc)
wholeIsNotOne ItIsOne impossible

isOne : (w : Whole) -> Dec (IsOne w)
isOne (W n prf) with (prf)
  isOne (W (S k) prf) | ItIsSucc with (k)
    isOne (W (S k) prf) | ItIsSucc | Z = Yes ItIsOne
    isOne (W (S k) prf) | ItIsSucc | (S j) = No wholeIsNotOne

data IsGreaterThanOne : Whole -> Type where
  IsGT1 : (LTE 2 (S n)) -> IsGreaterThanOne (W (S n) ItIsSucc)

wholeIsOne : Not (IsGreaterThanOne $ W (S Z) ItIsSucc)
wholeIsOne (IsGT1 (LTESucc LTEZero)) impossible
wholeIsOne (IsGT1 (LTESucc (LTESucc _))) impossible

decEqWholeNotEqual : (contra : (k = j) -> Void) -> (W (S k) ItIsSucc = W (S j) ItIsSucc) -> Void
decEqWholeNotEqual contra Refl = contra Refl

isGreaterThanOne : (w : Whole) -> Dec (IsGreaterThanOne w)
isGreaterThanOne (W n prf) with (prf)
  isGreaterThanOne (W (S k) prf) | ItIsSucc with (isLTE 2 (S k))
    isGreaterThanOne (W (S k) prf) | ItIsSucc | (Yes x) = Yes (IsGT1 x)
    isGreaterThanOne (W (S k) prf) | ItIsSucc | (No contra) with (k)
      isGreaterThanOne (W (S k) prf) | ItIsSucc | (No contra) | Z = No wholeIsOne
      isGreaterThanOne (W (S k) prf) | ItIsSucc | (No contra) | (S j) = Yes (IsGT1 (LTESucc (LTESucc LTEZero)))

DecEq Whole where
  decEq (W (S k) ItIsSucc) (W (S j) ItIsSucc) with (decEq k j)
    decEq (W (S j) ItIsSucc) (W (S j) ItIsSucc) | (Yes Refl) = Yes Refl
    decEq (W (S k) ItIsSucc) (W (S j) ItIsSucc) | (No contra) = No (decEqWholeNotEqual contra)

toNat : Whole -> Nat
toNat (W n prf) = n

fromNat : (x : Nat) -> {auto prf : IsSucc x} -> Whole
fromNat x {prf} = W x prf

data LTE : Whole -> Whole -> Type where
  IsLTE : (prf : LTE min max)
       -> LTE (W min prfA) (W mac prfB)

Show Whole where
  show (W n prf) = show n

Eq Whole where
  (W l prfL) == (W r prfR) = l == r

Cast Whole Integer where
  cast (W w prf) = toIntegerNat w

Ord Whole where
  compare (W l prfL) (W r prfR) = compare l r

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Test.Object

import Hedgehog
import Generics.Derive

import JS

%language ElabReflection

public export
record Address where
  constructor MkAddress
  street : String
  nr     : Bits32
  zip    : String
  city   : String

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

-- Direct JSON encoding
toStr : Address -> String
toStr s = #"{"street":\#{show s.street},"nr":\#{show s.nr},"zip":\#{show s.zip},"city":\#{show s.city}}"#

-- Encoding via `stringify`.
toJSON : Address -> String
toJSON a = let ps = [ ("street",Str a.street)
                    , ("nr", Num . fromInteger $ cast a.nr)
                    , ("zip", Str a.zip)
                    , ("city", Str a.city)
                    ]
            in stringify (pairs ps)

export
fromJSON : String -> Maybe Address
fromJSON s =
  do val <- parseMaybe s
     obj <- getObject val
     [| MkAddress (valueAt obj "street" >>= getStr)
                  (valueAt obj "nr" >>= map (fromInteger . cast) . getNum)
                  (valueAt obj "zip" >>= getStr)
                  (valueAt obj "city" >>= getStr) |]

--------------------------------------------------------------------------------
--          Generators
--------------------------------------------------------------------------------

plainString : Gen String
plainString = string (linear 1 10) alphaNum

export
addresses : Gen Address
addresses = [| MkAddress plainString
                         (bits32 $ linear 0 50)
                         plainString
                         plainString |]

--------------------------------------------------------------------------------
--          Properties
--------------------------------------------------------------------------------

prop_toJSON : Property
prop_toJSON = property $ do a <- forAll addresses
                            toStr a === toJSON a

prop_decode : Property
prop_decode = property $ do a <- forAll addresses
                            case parse (toJSON a) of
                                 Left e => do footnote (dispErr e)
                                              assert False
                                 Right _ => assert True

prop_roundTrip : Property
prop_roundTrip = property $ do a <- forAll addresses
                               Just a === fromJSON (toJSON a)

export
test : IO ()
test = ignore . checkGroup . withTests 100 $ MkGroup "Object" [
         ("prop_toJSON", prop_toJSON)
       , ("prop_decode", prop_decode)
       , ("prop_roundTrip", prop_roundTrip)
       ]


text:
module ProgramSynthSMT

import Data.Vect
import Data.String
import src.SMTLib
import src.Tensor

record VarPos (size : Nat) where
  constructor MkVar
  pos : Expr (BitVecT size)
  val : Expr (BitVecT size)

record Arg (size : Nat) where
  constructor MkArg
  isVar : Expr BoolT
  varPos : Expr (BitVecT size)
  instrPos : Expr (BitVecT size)
  val : Expr (BitVecT size)

record ArgName (size : Nat) where
  constructor MkArgName
  isVar : String
  varPos : String
  instrPos : String

record Instr (argsN : Nat) (size : Nat) where
  constructor MkInstr
  pos : Expr (BitVecT size)
  isConst : Expr BoolT
  constVal : Expr (BitVecT size)
  val : Expr (BitVecT size)
  op : Expr (BitVecT size)
  args : Vect argsN (Arg size)

record InstrName (argsN : Nat) (size : Nat) where
    constructor MkInstrName
    pos : Nat
    isConst : String
    constVal : String
    op : String
    args : Vect argsN (ArgName size)

record Op (argsN : Nat) (size : Nat) where
  constructor MkOp
  id : Integer
  func : Expr (BitVecT size) -> Vect argsN (Expr (BitVecT size)) -> Expr BoolT
  str : Vect argsN String -> String

createVarPos : Vect n (Expr (BitVecT size)) -> Vect n (VarPos size)
createVarPos {n} {size} vs = tabulate (\i => MkVar (bv (finToInteger i) size) (index i vs))

lookupVar : Expr (BitVecT size) -> Expr (BitVecT size) -> Vect n (VarPos size) -> Expr BoolT
lookupVar p v vs = or [ite' (p == pos vp) (v == val vp) (bool False) | vp <- vs]

createArgs : Vect n (Vect argsN (Expr BoolT)) -> Vect n (Vect argsN (Expr (BitVecT size))) -> Vect n (Vect argsN (Expr (BitVecT size))) ->  Vect n (Vect argsN (Expr (BitVecT size))) -> Vect n (Vect argsN (Arg size))
createArgs isVars vars instrs vals = tabulate (\i0 => tabulate (\i1 => MkArg (index i0 i1 isVars) (index i0 i1 vars) (index i0 i1 instrs) (index i0 i1 vals)))

createInstrs : Vect n (Expr BoolT) -> Vect n (Expr (BitVecT size)) -> Vect n (Expr (BitVecT size)) -> Vect n (Expr (BitVecT size)) -> Vect n (Vect argsN (Arg size)) -> Vect n (Instr argsN size)
createInstrs {size} isConsts constVals vals ops args = tabulate (\i => MkInstr (bv (finToInteger i) size) (index i isConsts) (index i constVals) (index i vals) (index i ops) (index i args))

lookupInstr : Expr (BitVecT size) -> Expr (BitVecT size) -> Vect n (Instr argsN size) -> Expr BoolT
lookupInstr p v instrs = or [ite' (p == pos instr) (v == val instr) (bool False) | instr <- instrs]

varNames : String -> Tensor [n] String
varNames name = toTensor $ tabulate (\i => name ++ "_" ++ show (finToNat i))

varNames' : String -> Tensor [n, m] String
varNames' name = toTensor $ tabulate (\i0 => tabulate (\i1 => name ++ "_" ++ show (finToNat i0) ++ "_" ++ show (finToNat i1)))

lookupOp : Expr (BitVecT size) -> Expr (BitVecT size) -> Vect argsN (Expr (BitVecT size)) -> Vect opsN (Op argsN size) -> Expr BoolT
lookupOp {size} opPos instrVal args ops = or [ite' (opPos == (bv (id op) size)) (func op instrVal args) (bool False) | op <- ops]

checkInstr : Vect n (Instr argsN size) -> Expr BoolT
checkInstr [] = bool True
checkInstr [instr] = and $ [constVal instr `bvule` bv 65000 size] ++ [isVar arg == bool True | arg <- args instr]
checkInstr (instr :: instrs) = and $ [constVal instr `bvule` bv 65000 size] ++ [or [instrPos arg == pos instr' | instr' <- instrs] | arg <- args instr] ++ [checkInstr instrs]

evalInstr : Vect opsN (Op argsN size) -> Vect varsN (VarPos size) -> Vect instrsN (Instr argsN size) -> Expr BoolT
evalInstr {argsN} ops vars instrs = and [ite' (isConst instr) (val instr == constVal instr) (and [assocArg vars instrs instr, lookupOp (op instr) (val instr) (map val $ args instr) ops]) | instr <- instrs]
  where
    assocArg : Vect varsN (VarPos size) -> Vect instrsN (Instr argsN size) -> Instr argsN size -> Expr BoolT
    assocArg vars instrs instr = and $ tabulate (\i => let arg = index i (args instr) in ite' (isVar arg) (lookupVar (varPos arg) (val arg) vars)
                                                                                (lookupInstr (instrPos arg) (val arg) instrs))

VarsN : Nat
VarsN = 1

ArgsN : Nat
ArgsN = 3

OpsN : Nat
OpsN = 17

BitSize : Nat
BitSize = 32

ops : Vect OpsN (Op ArgsN BitSize)
ops = let ops = the (Vect OpsN (Op ArgsN BitSize))
                [MkOp 0 (\r, arg => r == bvand (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " & " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvor (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " | " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvxor (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " ^ " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvnot (index 0 arg)) (\args => "~" ++ (index 0 args)),
                 MkOp 0 (\r, arg => ite' ((index 0 arg) == (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " == " ++ (index 1 args) ++ " ? (uint)1 : 0"),
                 MkOp 0 (\r, arg => r == bvsub (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " - " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvadd (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " + " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvmul (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " * " ++ (index 1 args)),
                 MkOp 0 (\r, arg => ite' ((index 0 arg) == bv 1 BitSize) (r == (index 1 arg)) (r == (index 2 arg))) (\args => (index 0 args) ++ " == 1 ? " ++ (index 1 args) ++ " : " ++ (index 2 args)),
                 MkOp 0 (\r, arg => ite' ((index 1 arg) == bv 0 BitSize) (r == bv 1 BitSize) (r == bvudiv (index 0 arg) (index 1 arg))) (\args => (index 1 args) ++ " == 0 ? (uint)1 : " ++ (index 0 args) ++ " / " ++ (index 1 args)),
                 --MkOp 0 (\r, arg => ite' ((index 1 arg) == bv 0 BitSize) (r == index 0 arg) (r == bvurem (index 0 arg) (index 1 arg))) (\args => (index 1 args) ++ " == 0 ? (uint)1 : " ++ (index 0 args) ++ " % " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvshl (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " << " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvlshr (index 0 arg) (index 1 arg)) (\args => (index 0 args) ++ " >> " ++ (index 1 args)),
                 MkOp 0 (\r, arg => r == bvneg (index 0 arg)) (\args => "-" ++ (index 0 args)),
                 MkOp 0 (\r, arg => ite' (bvule (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize)))  (\args => (index 0 args) ++ " <= " ++ (index 1 args) ++ " ? (uint)1 : 0"),
                 MkOp 0 (\r, arg => ite' (bvult (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " < " ++ (index 1 args) ++ " ? (uint)1 : 0"),
                 MkOp 0 (\r, arg => ite' (bvuge (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " >= " ++ (index 1 args) ++ " ? (uint)1 : 0"),
                 MkOp 0 (\r, arg => ite' (bvugt (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " > " ++ (index 1 args) ++ " ? (uint)1 : 0")] in
                 --MkOp 0 (\r, arg => ite' (bvsle (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " <= " ++ (index 1 args) ++ " ? 1 : 0"),
                 -- MkOp 0 (\r, arg => ite' (bvslt (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " < " ++ (index 1 args) ++ " ? 1 : 0"),
                 -- MkOp 0 (\r, arg => ite' (bvsge (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " >= " ++ (index 1 args) ++ " ? 1 : 0"),
                 -- MkOp 0 (\r, arg => ite' (bvsgt (index 0 arg) (index 1 arg)) (r == (bv 1 BitSize)) (r == (bv 0 BitSize))) (\args => (index 0 args) ++ " > " ++ (index 1 args) ++ " ? 1 : 0")] in
      zipWith (\op, i =>  record { id = cast i } op) ops (fromList [0..OpsN - 1])

varPosVal : Int -> Tensor [VarsN] String
varPosVal n = varNames $ "varPosVal" ++ show n

argIsVar : Tensor [ArgsN, instrsN] String
argIsVar = varNames' "argIsVar"

argVarPos : Tensor [ArgsN, instrsN] String
argVarPos = varNames' "argVarPos"

argInstrPos : Tensor [ArgsN, instrsN] String
argInstrPos = varNames' "argInstrPos"

argVal : Int -> Tensor [ArgsN, instrsN] String
argVal n = varNames' $ "argVal" ++ show n

instrVal : Int -> Tensor [instrsN] String
instrVal n = varNames $ "instrVal" ++ show n

instrOp : Tensor [instrsN] String
instrOp = varNames "instrOp"

instrIsConst : Tensor [instrsN] String
instrIsConst = varNames "isConst"

instrConstVal : Tensor [instrsN] String
instrConstVal = varNames "constVal"

instrNames : Vect instrsN (InstrName ArgsN BitSize)
instrNames = tabulate (\i => MkInstrName (finToNat i)
                                         (index i (toVect instrIsConst))
                                         (index i (toVect instrConstVal))
                                         (index i (toVect instrOp))
                                         (tabulate (\j => MkArgName (index i j (toVect argIsVar))
                                                                    (index i j (toVect argVarPos))
                                                                    (index i j (toVect argInstrPos)))))

eval : {prf : GTE instrsN 1} -> Int -> List (Expr (BitVecT BitSize), Expr (BitVecT BitSize) -> Expr BoolT) ->
       Tensor [ArgsN, instrsN] (Expr BoolT) -> Tensor [ArgsN, instrsN] (Expr (BitVecT BitSize)) ->
       Tensor [ArgsN, instrsN] (Expr (BitVecT BitSize)) -> Tensor [instrsN] (Expr (BitVecT BitSize)) ->
       Tensor [instrsN] (Expr BoolT) -> Tensor [instrsN] (Expr (BitVecT BitSize)) -> Smt ()
eval {instrsN} {prf} n [] argIsVar argVarPos argInstrPos instrOp instrIsConst instrConstVal = pure ()
eval {instrsN = S instrsN'} {prf = (LTESucc LTEZero)} n ((inp, outf) :: xs) argIsVar argVarPos argInstrPos instrOp instrIsConst instrConstVal =
    do vars <- declareVars (varPosVal n) (BitVecT BitSize)
       argVal <- declareVars (argVal {instrsN = S instrsN'} n) (BitVecT BitSize)
       instrVal <- declareVars (instrVal {instrsN = S instrsN'} n) (BitVecT BitSize)
       let vps = createVarPos (toVect vars)
       let args = createArgs (toVect argIsVar) (toVect argVarPos) (toVect argInstrPos) (toVect argVal)
       let instrs = createInstrs (toVect instrIsConst) (toVect instrConstVal) (toVect instrVal) (toVect instrOp) args
       assert $ evalInstr ops vps instrs
       assert $ val (index 0 vps) == inp
       r <- declareVar ("output" ++ show n) (BitVecT BitSize)
       assert $ outf r
       assert $ val (index 0 instrs) == r
       eval {prf = (LTESucc LTEZero)} (n + 1) xs argIsVar argVarPos argInstrPos instrOp instrIsConst instrConstVal
       pure ()

solver : {instrsN : Nat} -> {prf : GTE instrsN 1} -> List (Expr (BitVecT BitSize), Expr (BitVecT BitSize) -> Expr BoolT) -> Smt ()
solver {instrsN} {prf} xs =
         do setLogic "QF_BV"
            setOption ":timeout 600000"
            setOption ":parallel.enable true"
            setOption ":model_validate true"
            setOption ":pp.bv-literals false"
            let n = 0
            argIsVar <- declareVars (argIsVar {instrsN = instrsN}) BoolT
            argVarPos <- declareVars (argVarPos {instrsN = instrsN}) (BitVecT BitSize)
            argInstrPos <- declareVars (argInstrPos {instrsN = instrsN}) (BitVecT BitSize)
            instrOp <- declareVars (instrOp {instrsN = instrsN}) (BitVecT BitSize)
            instrIsConst <- declareVars (instrIsConst {instrsN = instrsN}) BoolT
            instrConstVal <- declareVars (instrConstVal {instrsN = instrsN}) (BitVecT BitSize)
            vars <- declareVars (varPosVal n) (BitVecT BitSize)
            argVal <- declareVars (argVal {instrsN = instrsN} n) (BitVecT BitSize)
            instrVal <- declareVars (instrVal {instrsN = instrsN} n) (BitVecT BitSize)
            let vps = createVarPos (toVect vars)
            let args = createArgs (toVect argIsVar) (toVect argVarPos) (toVect argInstrPos) (toVect argVal)
            let instrs = createInstrs (toVect instrIsConst) (toVect instrConstVal) (toVect instrVal) (toVect instrOp) args
            assert $ checkInstr instrs
            eval {prf = prf} (n + 1) xs argIsVar argVarPos argInstrPos instrOp instrIsConst instrConstVal
            checkSat
            getModel
            end

parseBool : String -> Maybe Bool
parseBool "true" = Just True
parseBool "false" = Just False
parseBool _ = Nothing

parseArgs : Model -> Vect n (ArgName size) -> Maybe (Vect n String)
parseArgs {n = Z} model args = Just []
parseArgs {n = (S n)} model ((MkArgName isVar varPos instrPos) :: args) =
  do isVarVal <- lookup isVar model
     isVar <- parseBool isVarVal
     varPosVal <- lookup varPos model
     instrPosVal <- lookup instrPos model
     args <- parseArgs model args
     pure $ [if isVar then "var" ++ varPosVal else "instr" ++ instrPosVal] ++ args

parseInstrs : Model -> Vect opsN (Op argsN size) -> Vect n (InstrName argsN size) -> Maybe (List String)
parseInstrs model ops [] = Just []
parseInstrs model ops ((MkInstrName pos isConst constVal opStr args) :: instrs) =
    do isConst <- lookup isConst model
       isConst <- parseBool isConst
       constVal <- lookup constVal model
       case isConst of
         True =>
          do args <- parseArgs model args
             instrs <- parseInstrs model ops instrs
             pure $ ["uint instr" ++ show pos ++ " = " ++ constVal ++ ";"] ++ instrs
         False =>
           do opVal <- lookup opStr model
              opId <- parseInteger {a = Integer} opVal
              op <- find (\op => id op == opId) ops
              args <- parseArgs model args
              instrs <- parseInstrs model ops instrs
              pure $ ["uint instr" ++ show pos ++ " = " ++ (str op args) ++ ";"] ++ instrs

equiv : Vect n (Expr a) -> Expr a -> Expr a -> (Expr a -> Vect n (Expr a) -> Expr BoolT) -> (Expr a -> Vect n (Expr a) -> Expr BoolT) -> Expr BoolT
equiv xs r r' f g = and [f r xs, g r' xs, not $ r == r']

testEquiv : Smt ()
testEquiv = let size = 64 in
            do setLogic "QF_BV"
               setOption ":pp.bv-literals false"
               setOption ":model_validate true"
               xs <- declareVars {f = Vect 3} ["a", "b", "c"] (BitVecT size)
               r <- declareVar "r" (BitVecT size)
               r' <- declareVar "_r" (BitVecT size)
               assert $ equiv xs r r' (\r, xs => r == ((((index 0 xs) `bvmul` (index 0 xs)) `bvmul` (index 0 xs)) `bvadd` (((index 1 xs) `bvmul` (index 1 xs)) `bvmul` (index 1 xs))))
                                      (\r, xs => r == (((index 2 xs) `bvmul` (index 2 xs)) `bvmul` (index 2 xs)))
               checkSat
               getModel
               end

runEquiv : IO ()
runEquiv = do r <- sat testEquiv
              case r of
                Nothing => do putStrLn "Error parsing result"
                Just (Sat, model) =>
                   do
                      putStrLn "sat"
                      putStrLn $ show model
                      pure ()
                Just (UnSat, _) => putStrLn "unsat"
                Just (Unknown, _) => putStrLn "unknown"

data' : List (Expr (BitVecT BitSize), Expr (BitVecT BitSize) -> Expr BoolT)
data' = let inp = example in
        map (\(a, b) => (bv a BitSize, \r => r == bv b BitSize)) inp
  where
    isPowerOfTwo : List (Integer, Integer)
    isPowerOfTwo = [(2, 1), (3, 0), (4, 1), (5, 0), (6, 0), (8, 1)]
    isEven : List (Integer, Integer)
    isEven = [(0, 1), (1, 0), (2, 1), (3, 0), (4, 1), (5, 0), (6, 1), (7, 0)]
    primes : List (Integer, Integer)
    primes = [(2, 3), (3, 5), (5, 7), (7, 11), (11, 13), (17, 19), (19, 23)]
    example : List (Integer, Integer)
    example = [(0, 2646464646)]

runSolver : (instrsN : Nat) -> {prf : GTE instrsN 1} -> IO ()
runSolver instrsN {prf} = do r <- sat $ solver {prf = prf} data'
                             --putStrLn $ "model: " ++ show r
                             case r of
                               Nothing => do putStrLn "Error parsing result"
                               Just (Sat, model) =>
                                  case parseInstrs {n = instrsN} model ops instrNames of
                                    Just instrs =>
                                      do putStrLn $ unlines $ reverse $ instrs
                                         pure ()
                                    Nothing => do putStrLn "Error parsing instrs"
                               Just (UnSat, _) => putStrLn "unsat"
                               Just (Unknown, _) => putStrLn "unknown"

run : (n : Nat) -> (instrsN : Nat) -> {auto prf : GTE instrsN 1} -> IO ()
run Z instrsN {prf = prf} = pure ()
run (S n) instrsN {prf = prf} = do putStrLn $ "n instrs: " ++ show instrsN
                                   runSolver {prf = prf} instrsN
                                   run n (S instrsN)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Aoc
import Data.List
import Data.SortedSet as S
%default total
-- this is slow

Point : Type
Point = (Integer, Integer)

||| Add two points.
(+~) : Point -> Point -> Point
(+~) (x,y) (x',y') = (x+x',y+y')
infixl 5 +~

Points : Type
Points = S.SortedSet Point

||| Filter a set.
filter : Ord k => (k -> Bool) -> SortedSet k -> SortedSet k
filter f = S.fromList . Data.List.filter f . S.toList

||| Apply "f" until the result stops changing, as judged by "eq".
partial
eqFixBy : (eq : a -> a -> Bool) -> (f : a -> a) -> (x : a) -> a
eqFixBy eq f x = let x' = f x in if eq x x' then x else eqFixBy eq f x'

||| Are two sets equal?
setEq : Ord k => S.SortedSet k -> S.SortedSet k -> Bool
setEq s1 s2 = S.toList s1 == S.toList s2

||| Apply a step function to the empty set until the result stops changing.
||| Then measure the size of the set.
partial
stableSize : (Points -> Points) -> Nat
stableSize f = length . S.toList $ eqFixBy setEq f S.empty

||| The 8 directions around (0,0).
directions : List Point
directions = [(-1,-1),( 0,-1),( 1,-1),
              (-1, 0),        ( 1, 0),
              (-1, 1),( 0, 1),( 1, 1)]

||| All immediate neighbor coordinates of a point.
neighbors1 : Point -> Points
neighbors1 p = S.fromList $ map (p+~) directions

||| Step to the next "occupied seats set" with a cellular automaton rule.
step : (neighbors : Point -> Points) -> (threshold : Nat) -> (seats : Points) -> (occupied : Points) -> Points
step neighbors threshold seats occupied = filter nowOccupied seats
  where
    nowOccupied : Point -> Bool
    nowOccupied p =
      let occ = (`S.contains` occupied)
          c = count occ (neighbors p)
      in if occ p then c < threshold else c == 0

||| Look for a point in a set in a given direction.
||| Give up when we're out of fuel.
seek : (fuel : Nat) -> Point -> Points -> Point -> Maybe Point
seek Z _ _ _ = Nothing
seek (S k) p ps dir =
  let p' = p +~ dir in
    if S.contains p' ps then Just p' else seek k p' ps dir

||| Seek for seats in all 8 directions.
||| (The fuel value "20" is eyeballed from the input ☠ merry christmas)
neighbors2 : (seats : Points) -> Point -> Points
neighbors2 seats p = S.fromList $ mapMaybe (seek 20 p seats) directions

partial
main : IO ()
main = do
  ls <- readLines
  let seats = S.fromList [(x,y) | (y,line) <- enumerate ls, (x,c) <- enumerate (unpack line), c == 'L']
  putStr "*   "; printLn $ stableSize (step neighbors1 4 seats)
  putStr "**  "; printLn $ stableSize (step (neighbors2 seats) 5 seats)