text:
module Js.HtmlUtils

import Js.HtmlTemplate
import Data.Vect

export
listCustomNS : String -> String -> List (BAttribute a f g) -> ((x:a) -> f x -> List (h x)) ->
                        BTemplate a h g -> BTemplate a f g
listCustomNS x = ListNode (Just x)

export
listCustom : String -> List (BAttribute a f g) -> ((x:a) -> f x -> List (h x)) ->
                        BTemplate a h g -> BTemplate a f g
listCustom = ListNode Nothing

namespace Dependent
  public export
  Template : (a:Type) -> (a->Type) -> (a->Type) -> Type
  Template = BTemplate

  public export
  Attribute : (a:Type) -> (a->Type) -> (a->Type) -> Type
  Attribute = BAttribute

  public export
  GuiRef : (a:Type) -> (a->Type) -> (a->Type)-> a -> Type
  GuiRef = BGuiRef

  export
  maybeOnSpanD : List (Attribute a f g) -> ((x:a)-> f x -> Maybe (h x)) -> BTemplate a h g -> BTemplate a f g
  maybeOnSpanD = MaybeNode "span"

  export
  listOnDivD : List (Attribute a f g) -> ((x:a) -> f x -> List (h x)) ->
                          BTemplate a h g -> BTemplate a f g
  listOnDivD = listCustom "div"

  export
  listOnDivIndexD : {h:a->Type} -> List (Attribute a f g) -> ((x:a) -> f x -> List (h x)) ->
                          BTemplate a (\x=> (Nat, h x)) g -> BTemplate a f g
  listOnDivIndexD attrs fn t = listOnDivD attrs (\x,y => let l = fn x y in zip [0..length l] l) t

  export
  vectOnDivIndex : {h:a->Type} -> List (Attribute a f g) -> (len : a->Nat) -> ((x:a) -> f x -> Vect (len x) (h x)) ->
                     BTemplate a (\x=>(Fin (len x), h x)) g -> BTemplate a f g
  vectOnDivIndex attrs len fn t = listOnDivD attrs (\x,y => let l = fn x y in toList $ zip range l) t

  export
  onclickD : ((x:a) -> f x -> g x) -> Attribute a f g
  onclickD = UnitEvent "click"

  export
  onchange : ((x:a) -> f x -> c x -> g x) -> InputAttribute a f g c
  onchange = OnChange

  export
  form : ((x:a) -> f x -> g x) -> List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
  form = FormNode

  infixl 4 >$<, <$>

  export
  (>$<) : ((x:a) -> h x -> f x) -> Template a f g -> Template a h g
  (>$<) a b = CMapNode a b

  export
  (<$>) : ((x:a) -> h x -> g x) -> Template a f h -> Template a f g
  (<$>) a b = MapNode a b

  export
  setVal : ((x:a) -> f x -> Maybe (c x)) -> InputAttribute a f g c
  setVal = SetVal

namespace Simple
  public export
  Template : {t:Type} -> Type -> Type -> Type
  Template {t} b c = BTemplate t (const b) (const c)

  public export
  Attribute : {t:Type} -> Type -> Type -> Type
  Attribute {t} b c = Attribute t (const b) (const c)

  public export
  GuiRef : Type -> Type -> Type
  GuiRef b c = BGuiRef () (const b) (const c) ()

  export
  maybeOnSpan : {t:Type} -> List (Attribute t (const b) (const c)) ->
                          (b -> Maybe d) -> BTemplate t (const d) (const c) -> BTemplate t (const b) (const c)
  maybeOnSpan attrs fn = MaybeNode "span" attrs (\_,y=> fn y)

  export
  listOnDiv : {t:Type} -> List (Attribute t (const b) (const c)) -> (b -> List d) ->
                          BTemplate t (const d) (const c) -> BTemplate t (const b) (const c)
  listOnDiv attrs fn = listCustom "div" attrs (\_,y=> fn y)

  export
  listOnDivIndex : {t:Type} -> List (Attribute t (const b) (const c)) -> (b -> List d) ->
                          BTemplate t (const (Nat, d)) (const c) -> BTemplate t (const b) (const c)
  listOnDivIndex {d} attrs fn = listOnDivIndexD {h=\_=>d} attrs (\_,y=> fn y)

  export
  onclick : {t:Type} -> (b -> c) -> Attribute t (const b) (const c)
  onclick fn = onclickD (\_,y=>fn y)

  export
  onShortPress : {t:Type} -> (b -> c) -> Attribute t (const b) (const c)
  onShortPress fn = EventShortPress (\_,y=>fn y)

  export
  onLongPress : {t:Type} -> (b -> c) -> Attribute t (const b) (const c)
  onLongPress fn = EventLongPress (\_,y=>fn y)

  export
  onclick' : {t:Type} -> c -> Attribute t (const b) (const c)
  onclick' x = onclick (const x)

  export
  onchange : {t:Type} -> (b -> c -> d) -> InputAttribute t (const b) (const d) (const c)
  onchange fn = OnChange (\_,x,y=> fn x y)

  export
  form : {t:Type} -> (b -> c) -> List (Attribute t (const b) (const c)) ->
            List (BTemplate t (const b) (const c)) -> BTemplate t (const b) (const c)
  form fn = FormNode (\_,x=>fn x)

  export
  form' : {t:Type} -> c -> List (Attribute t (const b) (const c)) ->
            List (BTemplate t (const b) (const c)) -> BTemplate t (const b) (const c)
  form' x = FormNode (\_,_=>x)

  export
  foldTemplate : ((x:a) -> s x) -> ((x:a) -> s x -> i x -> (s x, Maybe (r x))) -> ((x:a) -> (y:a) -> s x -> s y) ->
               BTemplate a s i -> List (FoldAttribute a f g s r) -> BTemplate a f g
  foldTemplate = FoldNode

  export
  setVal : {t:Type} -> (b -> Maybe c) -> InputAttribute t (const b) (const d) (const c)
  setVal fn = SetVal (\_,z=> fn z)

  export
  onchange' : {t:Type} -> (c -> d) -> InputAttribute t (const b) (const d) (const c)
  onchange' fn = OnChange (\_,_,x=> fn x)

export
groupAttribute : List (Attribute a f g) -> Attribute a f g
groupAttribute = GroupAttribute

export
textinput : List (InputAttribute a f g (const String)) ->
                BTemplate a f g
textinput = InputNode IText

export
customTextNS : String -> String -> List (Attribute a f g) -> Dyn (DPair a f) String -> BTemplate a f g
customTextNS x = TextNode (Just x)

export
customText : String -> List (Attribute a f g) -> Dyn (DPair a f) String -> BTemplate a f g
customText = TextNode Nothing

export
text : List (Attribute a f g) -> String -> Template a f g
text attrs txt = customText "span" attrs (DynConst txt)

export
textF : {t:Type} -> List (Attribute t (const a) (const b)) -> (a -> String) -> Template t (const a) (const b)
textF attrs txt = customText "span" attrs (DynA $ \(_**x)=> txt x)

export
textD : List (Attribute a f g) -> ((x:a) -> f x -> String) -> Template a f g
textD attrs txt = customText "span" attrs (DynA $ \(x**y)=>txt x y )

export
customNodeWidthPostProc : String -> (DomNode -> GuiCallback a f g -> JS_IO d, d -> JS_IO ()) ->
                            List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
customNodeWidthPostProc = CustomNode Nothing

export
customNodeWidthPostProcNS : String -> String -> (DomNode -> GuiCallback a f g -> JS_IO d, d -> JS_IO ()) ->
                            List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
customNodeWidthPostProcNS x = CustomNode (Just x)

export
customNode : String -> List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
customNode t = CustomNode Nothing t (\_,_=>pure (),\_=>pure ())

export
customNodeNS : String -> String -> List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
customNodeNS ns t = CustomNode (Just ns) t (\_,_=>pure (),\_=>pure ())

export
customStrAttr : String -> Dyn (DPair a f) String -> BAttribute a f g
customStrAttr = StrAttribute Nothing

export
customStrAttrNS : String -> String -> Dyn (DPair a f) String -> BAttribute a f g
customStrAttrNS x = StrAttribute (Just x)

export
img : List (Attribute a f g) -> String -> Template a f g
img attrs url = customNode "img" (customStrAttr "src" (DynConst url) ::attrs) []

export
imgF : {t:Type} -> List (Attribute t (const a) (const b) ) -> (a->String) -> Template t (const a) (const b)
imgF attrs url = customNode "img" (customStrAttr "src" (DynA $ \(_**x)=> url x) ::attrs) []

export
div : List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
div = customNode "div"

export
span : List (Attribute a f g) -> List (BTemplate a f g) -> BTemplate a f g
span = customNode "span"

export
button : List (Attribute a f g) -> String -> BTemplate a f g
button attrs x = customNode "button" attrs [text [] x]

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module HoareAsLogic

import Assn
import Expr
import Equiv
import Hoare
import Imp
import Logic
import Maps

%access public export

%default total

data HoareProof : Assertion -> Com -> Assertion -> Type where
  H_Skip : HoareProof p SKIP p
  H_Ass : HoareProof (AssignSub x a q) (x ::= a) q
  H_Seq : HoareProof p c q -> HoareProof q d r ->
          HoareProof p (do c; d) r
  H_If : HoareProof (\st => (p st, BAssn b st)) c1 q ->
         HoareProof (\st => (p st, Not (BAssn b st))) c2 q ->
         HoareProof p (CIf b c1 c2) q
  H_If1 : HoareProof (\st => (p st, BAssn b st)) c q ->
          (\st => (p st, Not (BAssn b st))) ->> q ->
          HoareProof p (CIf1 b c) q
  H_While : HoareProof (\st => (p st, BAssn b st)) c p ->
            HoareProof p (CWhile b c) (\st => (p st, Not (BAssn b st)))
  H_For : HoareProof p init q ->
          HoareProof (\st => (q st, BAssn cond st)) (do body; updt) q ->
          HoareProof p (CFor init cond updt body)
                       (\st => (q st, Not (BAssn cond st)))
  H_Repeat : HoareProof p c q -> (\st => (q st, Not (BAssn b st))) ->> p ->
             HoareProof p (CRepeat c b) (\st => (q st, BAssn b st))
  H_Consequence : HoareProof p' c q' -> (p ->> p') -> (q' ->> q) ->
                  HoareProof p c q

h_consequence_pre : HoareProof p' c q -> (p ->> p') -> HoareProof p c q
h_consequence_pre hp imp = H_Consequence hp imp assertImpliesRefl

h_consequence_post : HoareProof p c q' -> (q' ->> q) -> HoareProof p c q
h_consequence_post hp imp = H_Consequence hp assertImpliesRefl imp

sample_proof : HoareProof
                 (AssignSub X (X + 1) (AssignSub X (X + 2) (\st => st X = 3)))
                 (do X ::= X + 1; X ::= X + 2)
                 (\st => st X = 3)
sample_proof = H_Seq H_Ass H_Ass

hoare_proof_sound : HoareProof p c q -> HoareTriple p c q
hoare_proof_sound {q} H_Skip = hoare_skip q
hoare_proof_sound (H_Ass {q}) = hoare_assign q
hoare_proof_sound (H_Seq {p} {q} {r} hp1 hp2) =
  hoare_seq p q r (hoare_proof_sound hp2) (hoare_proof_sound hp1)
hoare_proof_sound (H_If {p} {q} {b} hpt hpf) =
  hoare_if p q (hoare_proof_sound hpt) (hoare_proof_sound hpf)
hoare_proof_sound (H_If1 {p} {q} hp imp) =
  hoare_if1 p q (hoare_proof_sound hp) imp
hoare_proof_sound (H_While {p} {b} hp) =
  hoare_while p (hoare_proof_sound hp)
hoare_proof_sound (H_For {p} {q} hp_init hp_body_updt) =
  hoare_for p q (hoare_proof_sound hp_init) (hoare_proof_sound hp_body_updt)
hoare_proof_sound (H_Repeat {p} {q} hp imp) =
  hoare_repeat p q (hoare_proof_sound hp) imp
hoare_proof_sound (H_Consequence {p} {q} {p'} {q'} hp p_imp q_imp) =
  hoare_consequence p p' q q' (hoare_proof_sound hp) p_imp q_imp

h_post_true_deriv : HoareProof p c (const ())
h_post_true_deriv {c = CSkip} = h_consequence_pre H_Skip (\_, _ => ())
h_post_true_deriv {c = (CAss _ _)} = h_consequence_pre H_Ass (\_, _ => ())
h_post_true_deriv {p} {c = (CSeq c1 c2)} =
  H_Seq (h_post_true_deriv {p=p} {c=c1}) (h_post_true_deriv {c=c2})
h_post_true_deriv {c = (CIf _ c1 c2)} =
  H_If (h_post_true_deriv {c=c1}) (h_post_true_deriv {c=c2})
h_post_true_deriv {c = (CIf1 _ c)} =
  H_If1 (h_post_true_deriv {c=c}) (\_, _ => ())
h_post_true_deriv {c = (CWhile _ c)} =
  H_Consequence (H_While {p=const ()} (h_post_true_deriv {c=c}))
                (\_, _ => ())
                (\_, _ => ())
h_post_true_deriv {p} {c = f@(CFor init _ updt body)} =
  h_consequence_post
    (H_For (h_post_true_deriv {p=p} {c=init})
           (h_post_true_deriv {c=assert_smaller f (do body; updt)}))
    (\_, _ => ())
h_post_true_deriv {c = (CRepeat c _)} =
  H_Consequence (H_Repeat (h_post_true_deriv {c=c}) (\_, _ => ()))
                (\_, _ => ())
                (\_, _ => ())

h_pre_false_deriv : HoareProof (const Void) c q
h_pre_false_deriv {c = CSkip} = h_consequence_pre H_Skip (\_, v => absurd v)
h_pre_false_deriv {c = (CAss x e)} = h_consequence_pre H_Ass (\_, v => absurd v)
h_pre_false_deriv {c = (CSeq c1 c2)} = H_Seq (h_pre_false_deriv {c=c1})
                                             (h_pre_false_deriv {c=c2})
h_pre_false_deriv {c = (CIf _ ct cf)} =
  H_If (h_consequence_pre (h_pre_false_deriv {c=ct}) (\_, (v, _) => v))
       (h_consequence_pre (h_pre_false_deriv {c=cf}) (\_, (v, _) => v))
h_pre_false_deriv {c = (CIf1 _ c)} =
  H_If1 (h_consequence_pre (h_pre_false_deriv {c=c}) (\_, (v, _) => v))
        (\_, (v, _) => absurd v)
h_pre_false_deriv {c = (CWhile _ c)} =
  h_consequence_post
    (H_While (h_consequence_pre (h_pre_false_deriv {c=c} {q=const Void})
                                (\_, (v, _) => v)))
    (\_, (v, _) => absurd v)
h_pre_false_deriv {c = f@(CFor init _ updt body)} =
  h_consequence_post
    (H_For (h_pre_false_deriv {c=init} {q=const Void})
           (h_consequence_pre
              (h_pre_false_deriv {c=assert_smaller f (do body; updt)})
              (\_, (v, _) => v)))
    (\_, (v, _) => absurd v)
h_pre_false_deriv {c = (CRepeat c _)} =
  h_consequence_post
    (H_Repeat (h_pre_false_deriv {c=c} {q=const Void}) (\_, (v, _) => v))
    (\_, (v, _) => absurd v)

WP : Com -> Assertion -> Assertion
WP c q = \s => (s' : State) -> CEval c s s' -> q s'

wp_is_precondition : HoareTriple (WP c q) c q
wp_is_precondition _ st' rel = \wp => wp st' rel

wp_is_weakest : HoareTriple p' c q -> (st : State) -> p' st -> WP c q st
wp_is_weakest ht st p'_st = \st', rel => ht st st' rel p'_st

hoare_proof_complete : HoareTriple p c q -> HoareProof p c q
hoare_proof_complete {c = CSkip} ht =
  h_consequence_post H_Skip (\st, p_st => ht st st E_Skip p_st)
hoare_proof_complete {c = (CAss x e)} ht =
  h_consequence_pre
    H_Ass (\st, q_st => ht st (t_update x (aeval st e) st) (E_Ass Refl) q_st)
hoare_proof_complete {q} {c = (CSeq c1 c2)} ht =
  H_Seq
    (hoare_proof_complete
      {c=c1} {q=WP c2 q}
      (\st1, _, r1, p_st, st3, r2 => ht st1 st3 (E_Seq r1 r2) p_st))
    (hoare_proof_complete {c=c2} (\_, st', rel, wp => wp st' rel))
hoare_proof_complete {c = (CIf b ct cf)} ht =
  H_If
    (hoare_proof_complete
      (\st, st', rel, (p_st, prf) => ht st st' (E_IfTrue prf rel) p_st))
    (hoare_proof_complete
      (\st, st', rel, (p_st, contra) =>
        ht st st' (E_IfFalse (bassn_eval_false contra) rel) p_st))
hoare_proof_complete {c = (CIf1 b c)} ht =
  H_If1
    (hoare_proof_complete
      (\st, st', rel, (p_st, prf) => ht st st' (E_If1True prf rel) p_st))
    (\st, (p_st, contra) =>
      ht st st (E_If1False (bassn_eval_false contra)) p_st)
hoare_proof_complete {c = (CWhile b c)} {q} ht =
  H_Consequence
    {p'=WP (CWhile b c) q}
    (H_While
      (hoare_proof_complete {c=c} $ \_, _, rel, (wp, prf), st'', rel' =>
        wp st'' (E_WhileLoop prf rel rel')))
    (\st, p_st, st', rel => ht st st' rel p_st)
    (\st, (wp, contra) => wp st (E_WhileEnd (bassn_eval_false contra)))
hoare_proof_complete {c = f@(CFor init cond updt body)} {q} ht =
  H_Consequence
    {p'=WP (CFor init cond updt body) q}
    (H_For
      {q=WP (CWhile cond (do body; updt)) q}
      (hoare_proof_complete $ \_, _, rel, wp, st'', rel' =>
        wp st'' (E_For rel rel'))
      (hoare_proof_complete
        {c=assert_smaller f (do body; updt)}
        (\_, _, rel, (wp, prf), st'', rel' =>
          wp st'' (E_WhileLoop prf rel rel'))))
    (\st, p_st, st', rel => ht st st' rel p_st)
    (\st, (wp, contra) => wp st (E_WhileEnd (bassn_eval_false contra)))
hoare_proof_complete {c = (CRepeat c b)} {q} ht =
  H_Consequence
    {p'=WP (CRepeat c b) q}
    (H_Repeat
      {q=WP (CWhile (not b) c) q}
      (hoare_proof_complete $
        \_, _, rel, wp, st'', rel' => wp st'' (E_Repeat rel rel'))
      (\st, (wp, contra), st', (E_Repeat r1 r2) =>
        let rel = snd (loop_unrolling {b=not b} {c=c} st st')
                      (E_IfTrue (cong {f=not} (fst not_true_iff_false contra))
                                (E_Seq r1 r2))
        in wp st' rel))
    (\st, p_st, st', rel => ht st st' rel p_st)
    (\st, (wp, prf) => wp st (E_WhileEnd (cong {f=not} prf)))

ext: idr


text:
module JS.Number

import Data.DPair
import Data.Bits
import JS.Inheritance
import JS.Marshall
import JS.Util
--------------------------------------------------------------------------------
--          Primitives
--------------------------------------------------------------------------------

%foreign "javascript:lambda:(a,b)=>a % b"
prim__mod : Double -> Double -> Double

%foreign "javascript:lambda:(a,b)=>Math.trunc(a / b)"
prim__div : Double -> Double -> Double

%foreign "javascript:lambda:v=>Number.isInteger(v)?v:Math.trunc(v)"
prim__toIntegral : AnyPtr -> AnyPtr

%foreign "javascript:lambda:(v,b)=>v >= b || v < (-b)?v%b:v"
prim__truncSigned : Double -> Double -> Double

%foreign "javascript:lambda:(v,b)=>v >= b || v < 0?Math.abs(v)%b:v"
prim__truncUnsigned : Double -> Double -> Double

%foreign "javascript:lambda:(a,b)=>a & b"
prim__and : Double -> Double -> Double

%foreign "javascript:lambda:(a,b)=>a | b"
prim__or : Double -> Double -> Double

%foreign "javascript:lambda:(a,b)=>a ^ b"
prim__xor : Double -> Double -> Double

%foreign "javascript:lambda:(a,b)=>a >> b"
prim__shr : Double -> Double -> Double

%foreign "javascript:lambda:(a,x,b)=>{ res = a << b; res & x ? res | (-x) : res & (x-1) }"
prim__shlSigned : Double -> Double -> Double -> Double

%foreign "javascript:lambda:(a,x,b)=> (a << b) & x"
prim__shlUnsigned : Double -> Double -> Double -> Double

%foreign "javascript:lambda:x=> Number.isInteger(x)?1:0"
prim__isInteger : AnyPtr -> Double

--------------------------------------------------------------------------------
--          JSInt64
--------------------------------------------------------------------------------

||| A 64-bit signed integer in the range [-9223372036854775808,9223372036854775807]
|||
||| This corresponds to the `Long Long` WebIDL type.
||| Internally, the number is represented by a
||| Javascript `Number`.
||| Note, that arithmetic operations on this type might result
||| in rounding errors, since values might be outside the range
||| of safe integral arithmetics (up to 2^53). Use this type only for
||| interacting with external API requiring values of this type.
export
data JSInt64 : Type where [external]

export
fromJSInt64 : JSInt64 -> Double
fromJSInt64 = believe_me

-- internal precondition: v is an integer
toJSInt64 : Double -> JSInt64
toJSInt64 = believe_me

-- internal precondition: v is an integer
truncToJSInt64 : Double -> JSInt64
truncToJSInt64 v = toJSInt64 (prim__truncSigned v 9223372036854775808.0)

export
Show JSInt64 where
  show = jsShow

export
Eq JSInt64 where
  (==) = (==) `on` fromJSInt64

export
Ord JSInt64 where
  compare = compare `on` fromJSInt64

export
Num JSInt64 where
  a + b = truncToJSInt64 $ fromJSInt64 a + fromJSInt64 b
  a * b = truncToJSInt64 $ fromJSInt64 a * fromJSInt64 b
  fromInteger = truncToJSInt64 . fromInteger

export
Neg JSInt64 where
  negate = truncToJSInt64 . negate . fromJSInt64
  a - b  = truncToJSInt64 $ fromJSInt64 a - fromJSInt64 b

export
Integral JSInt64 where
  a `div` b = toJSInt64 $ prim__div (fromJSInt64 a) (fromJSInt64 b)
  a `mod` b = toJSInt64 $ prim__mod (fromJSInt64 a) (fromJSInt64 b)

export
ToFFI JSInt64 JSInt64 where toFFI = id

export
FromFFI JSInt64 JSInt64 where fromFFI = Just

export
SafeCast JSInt64 where
  safeCast = bounded (-9223372036854775808) 9223372036854775808

--------------------------------------------------------------------------------
--          JSBits64
--------------------------------------------------------------------------------

||| A 64-bit unsigned integer in the range [0,18446744073709551615].
|||
||| This corresponds to the `Unsigned Long Long` WebIDL type.
||| Internally, the number is represented by a Javascript `Number`.
||| Note, that this type is therefore susceptible to
||| rounding errors, since values might be outside the range
||| of safe integral arithmetics (up to 2^53). Use this type only for
||| interacting with external API requiring values of this type.
export
data JSBits64 : Type where [external]

export
fromUInt64 : JSBits64 -> Double
fromUInt64 = believe_me

-- internal precondition: v is a non-negative integer
toUInt64 : Double -> JSBits64
toUInt64 = believe_me

-- internal precondition: v is an integer
truncToUInt64 : Double -> JSBits64
truncToUInt64 v = toUInt64 (prim__truncUnsigned v 18446744073709551616.0)

export
Show JSBits64 where
  show = jsShow

export
Eq JSBits64 where
  (==) = (==) `on` fromUInt64

export
Ord JSBits64 where
  compare = compare `on` fromUInt64

export
Num JSBits64 where
  a + b = truncToUInt64 $ fromUInt64 a + fromUInt64 b
  a * b = truncToUInt64 $ fromUInt64 a * fromUInt64 b
  fromInteger = truncToUInt64 . fromInteger

export
Integral JSBits64 where
  a `div` b = toUInt64 $ prim__div (fromUInt64 a) (fromUInt64 b)
  a `mod` b = toUInt64 $ prim__mod (fromUInt64 a) (fromUInt64 b)

export
ToFFI JSBits64 JSBits64 where toFFI = id

export
FromFFI JSBits64 JSBits64 where fromFFI = Just

export
SafeCast JSBits64 where
  safeCast = bounded 0 18446744073709551615


text:
module Erlang.Debug

import Erlang

%default total

||| Print the underlying value using `io:format/2`.
export
erlPrintLn : HasIO io => a -> io ()
erlPrintLn x = do
  ignore $ pure $ erlUnsafeCall ErlTerm "io" "format" ["~p~n", the (ErlList _) [MkRaw x]]

||| Print the underlying value using `io:format/2`, and return the given value.
|||
||| This function is unsafe as it breaks referential transparency.
export
erlInspect : a -> a
erlInspect x = unsafePerformIO $ do
  erlPrintLn x
  pure x

export
erlPrintMemory : HasIO io => io ()
erlPrintMemory =
  erlPrintLn (erlUnsafeCall ErlTerm "erlang" "memory" [])

-- TIME PROFILER

public export
data AnalyzeFilter = FilterByCalls Integer | FilterByTime Double

public export
data AnalyzeSort = SortByTime | SortByCalls | SortByMFA

public export
record AnalyzeOpts where
  constructor MkAnalyzeOpts
  filters : List AnalyzeFilter
  sort : Maybe AnalyzeSort

export
erlDefaultAnalyzeOpts : AnalyzeOpts
erlDefaultAnalyzeOpts = MkAnalyzeOpts [] Nothing

ToErlTerm AnalyzeFilter where
  toErlTerm (FilterByCalls limit) = toErlTerm $ MkTuple2 (MkAtom "calls") limit
  toErlTerm (FilterByTime limit) = toErlTerm $ MkTuple2 (MkAtom "time") limit

ToErlTerm AnalyzeSort where
  toErlTerm SortByTime = toErlTerm $ MkAtom "time"
  toErlTerm SortByCalls = toErlTerm $ MkAtom "calls"
  toErlTerm SortByMFA = toErlTerm $ MkAtom "mfa"

ToErlTerm AnalyzeOpts where
  toErlTerm (MkAnalyzeOpts filters sort) =
    let filterOpt = MkTuple2 (MkAtom "filter") (toErlTerm <$> filters)
        sortOpt = MkTuple2 (MkAtom "sort") . toErlTerm <$> sort
    in toErlTerm (filterOpt :: toList sortOpt)

export
erlRunTimeProfiler : HasIO io => AnalyzeOpts -> IO () -> io ()
erlRunTimeProfiler opts prog = do
  ignore $ pure $ erlUnsafeCall ErlTerm "eprof" "start" []
  ignore $ pure $ erlUnsafeCall ErlTerm "eprof" "start_profiling" [the (ErlList _) [!erlSelf]]
  liftIO prog
  ignore $ pure $ erlUnsafeCall ErlTerm "eprof" "stop_profiling" []
  ignore $ pure $ erlUnsafeCall ErlTerm "eprof" "analyze" [MkAtom "total", toErlTerm opts]
  ignore $ pure $ erlUnsafeCall ErlTerm "eprof" "stop" []


text:
module Addition.Lemmas.Carry

import Common.Util
import Specifications.DiscreteOrderedGroup
import Proofs.GroupCancelationLemmas
import Proofs.GroupCancelMisc
import Proofs.GroupTheory
import Proofs.TranslationInvarianceTheory
import Proofs.Interval

%default total
%access export

||| Adhoc lemma.
||| Start with `computeCarry` to understand where it fits.
shiftToLeft : {(+) : Binop s} ->
  PartiallyOrderedGroupSpec (+) _ neg leq ->
    (u,a,x : s) ->
    Between leq (neg (u + u), neg u) x ->
    Between leq (a + neg u, a) (a + u + x)
shiftToLeft spec u a x given = rewriteBetween o2 o3 o1 where
  o1 : Between leq (a + u + neg (u + u), a + u + neg u) (a + u + x)
  o1 = translateIntervalL (invariantOrder spec) (a + u) given
  o2 : a + u + neg (u + u) = a + neg u
  o2 = groupCancelMisc2 (group spec) a u _
  o3 : a + u + neg u = a
  o3 = groupCancel3bis (group spec) a u

||| Adhoc lemma.
||| Start with `computeCarry` to understand where it fits.
shiftLeftToSymRange : {(+) : Binop s} ->
  PartiallyOrderedGroupSpec (+) _ neg leq ->
    (u,a,x : s) ->
    leq a (u + neg a) ->
    Between leq (neg (u + u), neg u) x ->
    InSymRange leq neg (u + neg a) (a + u + x)
shiftLeftToSymRange {s} spec u a x bound given = o4 where
  sx : s
  sx = a + u + x
  o1 : Between leq (a + neg u, a) sx
  o1 = shiftToLeft spec u a x given
  o2 : Between leq (a + neg u, u + neg a) sx
  o2 = weakenR (order spec) bound o1
  o3 : neg (u + neg a) = a + neg u
  o3 = groupInverseAntiInverse (group spec) u a
  o4 : Between leq (neg (u + neg a), u + neg a) sx
  o4 = rewriteBetween (sym o3) Refl o2

||| Adhoc lemma.
||| Start with `computeCarry` to understand where it fits.
||| Derived from `shiftLeftToSymRange` using symmetry.
shiftRightToSymRange : {(+) : Binop s} ->
  PartiallyOrderedGroupSpec (+) _ neg leq ->
    (u,a,x : s) ->
    leq a (u + neg a) ->
    Between leq (u, u + u) x ->
    InSymRange leq neg (u + neg a) (x + neg (a + u))
shiftRightToSymRange spec u a x bound given = rewrite sym o2 in o1 where
  o1 : InSymRange leq neg (u + neg a) (neg (a + u + neg x))
  o1 = invertSymRange spec $
       shiftLeftToSymRange spec u a (neg x) bound $
       invertBetween spec given
  o2 : neg (a + u + neg x) = x + neg (a + u)
  o2 = groupInverseAntiInverse (group spec) (a + u) x

||| Lemma: turn an interval into a proper SymRange.
toSymRange : {(+) : Binop s} ->
  PartiallyOrderedGroupSpec (+) _ neg leq ->
  isAbelian (+) ->
    Between leq (a + neg b, neg a + b) x ->
    InSymRange leq neg (b + neg a) x
toSymRange spec abel =
  rewriteBetween (sym $ groupInverseAntiInverse (group spec) _ _) (abel _ _)

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
-- -------------------------------------------------------------- [ Reader.idr ]
-- Module      : UML.Reader
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
--
-- Reading Utilities
-- --------------------------------------------------------------------- [ EOH ]
module UML.Reader

import public Effects
import public Effect.Exception
import public Effect.File

import Lightyear
import Lightyear.Strings

import UML.Class
import UML.Sequence
import UML.Deployment
import UML.Component
import UML.Code

import UML.Types

import public UML.Utils.Reading

%access public
-- ------------------------------------------------------------------------ [  ]
private
doParse : Parser UML -> String -> {[EXCEPTION String]} Eff UML
doParse p src = case parse p src of
    Left err    => raise err
    Right model => pure model

||| Read a UML file from string.
readUMLString : UMLTy
              -> String
              -> {[EXCEPTION String]} Eff UML
readUMLString CLAZZ      = doParse classModel
readUMLString SEQUENCE   = doParse sequenceModel
readUMLString DEPLOYMENT = doParse deploymentModel
readUMLString COMPONENT  = doParse componentModel

||| Read a UML model from a file
readUMLFile : UMLTy
            -> String
            -> {[EXCEPTION String, FILE_IO ()]} Eff UML
readUMLFile ty fname = do
    src <- readFile fname
    model <- readUMLString ty src
    pure model
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Verified.Functor.List

import Verified.Functor

instance VerifiedFunctor List where
  functorIdentity [] = Refl
  functorIdentity (x :: xs) =
    let IHxs = functorIdentity xs in ?lemma1
  functorComposition [] g1 g2 = Refl
  functorComposition (x :: xs) g1 g2 =
    let IHxs = functorComposition xs g1 g2 in ?lemma2

---------- Proofs ----------

Verified.Functor.List.lemma2 = proof
  intros
  rewrite IHxs
  exact Refl

Verified.Functor.List.lemma1 = proof
  intros
  rewrite IHxs
  exact Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module ArgParse.Parser.API

import Data.String.Views

import public Text.Parser
import ArgParse.Lexer

%default total
%access export

public export
Rule : Type -> Type
Rule ty = Grammar (TokenData Token) True ty

public export
EmptyRule : Type -> Type
EmptyRule ty = Grammar (TokenData Token) False ty

-- Some basic parsers used by all the intermediate forms

export
shortFlag : Rule String
shortFlag
    = terminal (\x => case tok x of
                           SFlag f => Just (substr 1 (length f) f)
                           _     => Nothing)

export
longFlag : Rule String
longFlag
    = terminal (\x => case tok x of
                           LFlag f => Just (substr 2 (length f) f)
                           _       => Nothing)

export
arg : Rule String
arg = terminal
  (\x => case tok x of
           Arg s => Just (trim s)
           _     => Nothing)

export
equals : Rule ()
equals = terminal
  (\x => case tok x of
           Equals _ => Just ()
           _        => Nothing)

export
quoted : Rule String
quoted = terminal
    (\x => case tok x of
             Quoted s => Just $ rmQuotes s
             _        => Nothing)
  where
    rmQuotes : String -> String
    rmQuotes xs = pack $ filter (not . (==) '"') (unpack xs)

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

max_stars_repo_name: jfdm/idris-argparse

max_issues_repo_name: jfdm/idris-argparse

max_forks_repo_name: jfdm/idris-argparse


text:
factorial : (n : Nat) -> Nat
factorial Z = 1
factorial n@(S k) = n * factorial k

testFactorial1 : factorial 3 = 6
testFactorial1 = Refl
testFactorial2 : factorial 5 = 10 * 12
testFactorial2 = Refl

beq_nat : (n, m : Nat) -> Bool
beq_nat Z Z = True
beq_nat Z (S j) = False
beq_nat (S k) Z = False
beq_nat (S k) (S j) = beq_nat k j

leb : (n, m : Nat) -> Bool
leb Z m = True
leb (S k) Z = False
leb (S k) (S j) = leb k j

blt_nat : (n, m : Nat) -> Bool
blt_nat n m = leb n m && not (beq_nat n m)

test_blt_nat_1 : blt_nat 2 2 = False
test_blt_nat_1 = Refl
test_blt_nat_2 : blt_nat 2 4 = True
test_blt_nat_2 = Refl
test_blt_nat_3 : blt_nat 4 2 = False
test_blt_nat_3 = Refl


text:
module Client.Action.FetchDeps

import Client.Action.BuildDeps
import Client.Action.CacheDeps
import Client.Action.Pull
import Client.Server
import Data.List
import Data.SortedSet as Set
import Extra.String
import Inigo.Async.Base
import Inigo.Async.Fetch
import Inigo.Async.FS
import Inigo.Async.Git
import Inigo.Async.Package
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Package.PackageDeps
import Inigo.Paths
import Inigo.Util.Url.Url
import SemVar
import SemVar.Sat

getPackageDepTree : Server -> String -> String -> Promise PackageDepTree
getPackageDepTree server packageNS packageName =
  do
    let url = toString (fromHostPath (host server) (getPackageDepTreeUrl packageNS packageName))
    log ("Requesting " ++ url ++ "...")
    contents <- fetch url
    Right packageDepTree <- lift (parsePackageDepTree contents)
      | Left err => reject ("Invalid package dep tree: " ++ err)
    pure packageDepTree

-- Responsible for pulling deps based on package conf

-- Note: we're currently going to ignore sub-deps entirely

splitDep : List String -> Maybe (String, String)
splitDep (ns :: dep) = Just (ns, join "." dep)
splitDep _ = Nothing

removeDups : Ord a => List a -> List a
removeDups = Set.toList . Set.fromList

collect : Bool -> PackageDepTree -> List VersionNode
collect includeDevDeps depTree =
  concat $ map (\(pkg, pkgDeps) =>
    map (\(version, pkgDep) =>
      (pkg, version, (deps pkgDep) ++ (if includeDevDeps then (dev pkgDep) else []))
    ) pkgDeps
  ) depTree

-- Okay, here's where the fun begins
-- We're going to grab all sub-dep trees via our new deps endpoint
-- and then we're going to cull dups and then pass it to semvar sat to try
-- and return us what deps we should fetch!
fetchDeps : Server -> Bool -> Bool -> Package -> Promise (List (String, Package))
fetchDeps server includeDevDeps build pkg =
  do
    -- We have a list of deps, so we basically just need to `pull` each
    -- but we need to know the versions...
    -- Let's start by just pulling the latest of each
    let allDeps = deps pkg ++ (if includeDevDeps then (devDeps pkg) else [])
    let depNames = map fst allDeps
    let splitDeps = mapMaybe splitDep depNames

    depTree <- all $ map (uncurry $ getPackageDepTree server) splitDeps
    let versionNodes = collect includeDevDeps (concat depTree)
    log ("Package Dep Tree: " ++ (show versionNodes))
    Right sat <- lift $ satisfyAll versionNodes allDeps
      | Left err => reject ("Error satisfying contraints: " ++ err)
    log ("Sat: " ++ (show sat))

    all $ map pullDep sat
    -- TODO: We should only build things which have changed
    -- TODO: How do we know what's changed?
    -- if build
    --   then buildDeps
    --   else pure ()
  where
    pullDep : (List String, Version) -> Promise (String, Package)
    pullDep (pkg, version) =
      case splitDep pkg of
        Nothing =>
          reject ("Invalid dep: " ++ show pkg)

        Just (packageNS, packageName) =>
          do
            pull server packageNS packageName (Just version)
            let src = inigoDepDir </> joinPath pkg
            pkg <- readPackage src
            pure (src, pkg)

||| Get all elems of the left list not present in the right list
total
difference : Eq a => List a -> List a -> List a
difference xs [] = xs
difference xs (y :: ys) = difference (delete y xs) ys

fetchExtraDeps : Bool -> Bool -> Package -> Promise (List (String, Package))
fetchExtraDeps devDeps build pkg = do
    deps <- fetchDeps [] pkg.extraDeps
    foldlM getExtraDepPkg [] deps
  where
    getSubDirPkg : String -> List (String, Package) -> String -> Promise (List (String, Package))
    getSubDirPkg depDir pkgs subDir = do
        let srcDir = depDir </> subDir
        pkg <- readPackage srcDir
        if any ((== pkg) . snd) pkgs
            then pure pkgs
            else pure ((srcDir, pkg) :: pkgs)

    getExtraDepPkg : List (String, Package) -> ExtraDep -> Promise (List (String, Package))
    getExtraDepPkg pkgs dep@(MkExtraDep _ _ _ subDirs) =
        foldlM (getSubDirPkg $ getExtraDepDir dep) pkgs subDirs

    genIPkg : String -> String -> Promise Package
    genIPkg dest subDir = do
        let buildDir = joinPath (".." <$ splitPath (dest </> subDir)) </> "build"
        let pkgdir = dest </> subDir
        let iPkgFile = dest </> subDir </> inigoIPkgPath
        pkg <- readPackage pkgdir
        fs_writeFile iPkgFile $ generateIPkg False (Just buildDir) pkg
        pure pkg

    fetchExtraDep : ExtraDep -> Promise (List Package)
    fetchExtraDep pkg@(MkExtraDep Git commit url subDirs) = do
        let dest = getExtraDepDir pkg
        log "Downloading package from \"\{url}\""
        ignore $ git_downloadTo url (Just commit) dest
        traverse (genIPkg dest) subDirs
    fetchExtraDep pkg@(MkExtraDep SubDir _ url subDirs) = do
        let dest = getExtraDepDir pkg
        log "Checking packages in \"\{url}\""
        traverse (genIPkg dest) subDirs

    fetchDeps : List ExtraDep -> List ExtraDep -> Promise (List ExtraDep) -- if this is too slow, use SortedSet
    fetchDeps done [] = pure done
    fetchDeps done (MkExtraDep _ _ _ [] :: todo) = fetchDeps done todo
    fetchDeps done (pkg@(MkExtraDep _ _ _ subDirs0) :: todo) = case find (eqIgnoreSubDirs pkg) done of
        Nothing => do -- doesn't exist yet, download and add dependencies
            pkgs <- fetchExtraDep pkg
            let todo' = foldl (\acc, pkg => pkg.extraDeps ++ acc) todo pkgs
            fetchDeps (pkg :: done) todo'
        Just pkg@(MkExtraDep method info url subDirs1) => case difference subDirs0 subDirs1 of
            [] => fetchDeps done todo -- no missing subdirs, move on
            missing => do
                let dest = getExtraDepDir pkg
                pkgs <- traverse (genIPkg dest) missing
                let todo' = foldl (\acc, pkg => pkg.extraDeps ++ acc) todo pkgs
                let done' = MkExtraDep method info url (missing ++ subDirs0) :: filter (not . eqIgnoreSubDirs pkg) done
                fetchDeps done' todo
export
fetchAllDeps : Server -> Bool -> Bool -> Promise ()
fetchAllDeps server devDeps build = do
    pkg <- currPackage
    deps <- fetchDeps server devDeps build pkg
    extraDeps <- fetchExtraDeps devDeps build pkg
    let allDeps = deps ++ extraDeps
    writeDepCache allDeps

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module IdvPaths

import public IdvPaths.Generated

import Data.Version
import System.Path
import System.Directory.Extra
import System
import System.File

import Interp

export
idrisRepoURL : String
idrisRepoURL = "https://github.com/idris-lang/Idris2.git"

export
idrisLspRepoURL : String
idrisLspRepoURL = "https://github.com/idris-community/idris2-lsp.git"

export
idrisLspBranchName : (idrisVersion : Version) -> String
idrisLspBranchName idrisVersion =
  "idris2-\{dropPrerelease idrisVersion}"

public export
data BuildTarget = Idris | LSP

export
relativeCheckoutPath : (target : BuildTarget) -> String
relativeCheckoutPath Idris = "idris_checkout"
relativeCheckoutPath LSP = "lsp_checkout"

export
relativeVersionsPath : String
relativeVersionsPath = "versions"

export
relativeBinPath : String
relativeBinPath = "bin"

export
relativeLibPath : Version -> String
relativeLibPath version = "idris2-\{dropPrerelease version}"

idrisBinName : String
idrisBinName = "idris2"

||| The full path & executable name of the Idris 2
||| binary within the Idv directory (which is a symlink
||| pointing at the actual installed binary of whichever
||| version of Idris 2 is currently selected).
export
idrisSymlinkedPath : String
idrisSymlinkedPath =
  idvLocation </> relativeBinPath </> idrisBinName

idrisLspBinName : String
idrisLspBinName = "idris2-lsp"

||| The full path & executable name of the Idris 2
||| LSP binary within the Idv directory. This is a
||| symlink to the version of the LSP executable that
||| is currently selected.
export
idrisLspSymlinkedPath : String
idrisLspSymlinkedPath =
  idvLocation </> relativeBinPath </> idrisLspBinName

||| Get the name of the directory where the given version is installed
||| This is the directory relative to `idvLocation`/`relativeVersionsPath`
export
relativeVersionDirName : Version -> String
relativeVersionDirName (V major minor patch Nothing _) = "\{show major}_\{show minor}_\{show patch}"
relativeVersionDirName (V major minor patch (Just pre) _) = "\{show major}_\{show minor}_\{show patch}-\{pre}"

||| The full path where the given version is installed.
export
versionPath : Version -> String
versionPath version =
  idvLocation </> relativeVersionsPath </> (relativeVersionDirName version)

||| The full path where libraries for the given version are installed.
export
libPath : Version -> String
libPath version =
  idvLocation </> relativeVersionsPath </> (relativeVersionDirName version) </> (relativeLibPath version)

||| The path where the Idris 2 API package is installed for the
||| version (if it has been installed).
||| e.g. ~/.idv/versions/0_4_0/idris2-0.4.0/idris2-0.4.0
export
idrisApiLibPath : Version -> String
idrisApiLibPath version =
  (libPath version) </> (relativeLibPath version)

||| The build prefix (PREFIX) to use when making and installing the
||| the given version of the Idris 2 compiler.
export
buildPrefix : Version -> String
buildPrefix = versionPath

||| The full path & executable name of the Idris 2
||| binary within the _versions_ subdirectory of the
||| Idv directory. This is the _actual_ installed binary
||| for the given version that is in turn symlinked to
||| by `idrisSymlinkedPath` when the given version is
||| selected.
export
installedIdrisPath : Version -> String
installedIdrisPath version =
  versionPath version </> relativeBinPath </> idrisBinName

||| The full path & executable name of the Idris 2
||| LSP binary within the _versions_ subdirectory of the
||| Idv directory. This is the _actual_ installed binary
||| for the given version that is in turn symlinked to
||| by `idrisLspSymlinkedPath` when the given version is
||| selected.
export
installedLspPath : Version -> String
installedLspPath version =
  versionPath version </> relativeBinPath </> idrisLspBinName

||| The install location of the system copy of Idris 2.
||| If Idris 2 cannot be located on the system (i.e.
||| outside of the Idv versions directory) this function
||| returns Nothing.
export
systemIdrisPath : HasIO io => io (Maybe String)
systemIdrisPath = do
  Nothing <- checkLocation =<< getEnv "IDRIS2"
    | Just envOverride => pure $ Just envOverride
  checkLocation =<< defaultPath
    where
      defaultPath : io (Maybe String)
      defaultPath = pathExpansion defaultIdris2Location

      checkLocation : Maybe String -> io (Maybe String)
      checkLocation Nothing     = pure Nothing
      checkLocation (Just path) = pure $ guard !(exists path) *> Just path

||| The install location of the system copy of the LSP server.
||| If Idris 2 cannot be located on the system (i.e.
||| outside of the Idv versions directory) this function
||| returns Nothing.
export
systemIdrisLspPath : HasIO io => io (Maybe String)
systemIdrisLspPath = do
  Just idris2Exec <- do
      Nothing <- checkLocation =<< getEnv "IDRIS2"
        | Just envOverride => pure $ Just envOverride
      checkLocation =<< defaultPath
    | Nothing => pure Nothing
  let Just dir = parent idris2Exec
    | Nothing => pure Nothing
  let lspExec = dir </> idrisLspBinName
  pure $ guard !(exists lspExec) *> Just lspExec
    where
      defaultPath : io (Maybe String)
      defaultPath = pathExpansion defaultIdris2Location

      checkLocation : Maybe String -> io (Maybe String)
      checkLocation Nothing     = pure Nothing
      checkLocation (Just path) = pure $ guard !(exists path) *> Just path

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module Main

import Data.Hash

main : IO ()
main = do printLn $ hash (the Bits8 3)
          printLn $ hash (the (List Bits8) [3])
          printLn $ hash "hello world"
          printLn $ hash 'a'
          printLn $ hash (the Bits8 3)
          printLn $ hash (the Bits16 3)
          printLn $ hash (the Bits32 3)
          printLn $ hash (the Bits64 3)
          printLn $ hash (the Int 3)
          printLn $ hash (the Integer 3)
          printLn $ divB8 10 255
          printLn $ divB16 10 65535
          printLn $ divB32 10 4294967295
          printLn $ divB64 10 18446744073709551615

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
||| Core types and utility functions for all things related to combat
module Bautzen.Combats

import Bautzen.GameUnit
import Bautzen.Pos

import Data.Maybe.Extra

import Data.Fin
import Data.List
import Data.Nat
import Data.Vect

%default total

||| Combat result as steps lost by attacker and defender.
public export
record Losses where
  constructor (/>)

  ||| Steps lost by attacker
  attackerLoss : Nat

  ||| Steps lost by defender. Can be transformed in hexes of retreat.
  defenderLoss : Nat

infix 1 />

public export
Show Losses  where
  show (attackerLoss /> defenderLoss) =
    show attackerLoss ++ "/" ++ show defenderLoss

public export
record EngagedUnits where
  constructor MkEngagedUnits
  base : List (GameUnit, Pos)
  tacticalSupport : List (GameUnit, Pos)
  strategicSupport : Nat

public export
Show EngagedUnits where
  show (MkEngagedUnits base tacticalSupport strategicSupport) =
    "MkEngagedUnits base="++ show base ++
    ", tacticalSupport=" ++ show tacticalSupport ++
    ", strategicSupport=" ++ show strategicSupport

public export
record CombatState where
  constructor MkCombatState
  combatHex : Pos
  attackers : EngagedUnits
  defenders : EngagedUnits
  losses : Maybe Losses

public export
Show CombatState where
  show (MkCombatState combatHex attackers defenders losses) =
    "MkCombatState hex=" ++ show combatHex ++
    ", attacker=" ++ show attackers ++
    ", defender="++ show defenders ++
    ", losses=" ++ show losses

||| Combat resolution table.
|||
||| The table is transposed w.r.t. the actual rules booklet
public export
CombatTable : Vect 8 (Vect 8 Losses)
CombatTable =
  [ [ 3 /> 0, 3 /> 0, 3 /> 0, 2 /> 0 , 2 /> 1 , 2 /> 1 , 1 /> 1 , 0 /> 1 ]
  , [ 2 /> 0, 2 /> 0, 1 /> 0, 1 /> 0 , 2 /> 1 , 2 /> 2 , 2 /> 2 , 1 /> 2 ]
  , [ 1 /> 0, 1 /> 0, 1 /> 0, 1 /> 1 , 1 /> 1 , 1 /> 2 , 0 /> 2 , 0 /> 2 ]
  , [ 1 /> 0, 1 /> 0, 1 /> 1, 1 /> 2 , 1 /> 2 , 1 /> 2 , 1 /> 2 , 1 /> 3 ]
  , [ 1 /> 1, 1 /> 1, 1 /> 2, 1 /> 2 , 1 /> 2 , 1 /> 3 , 1 /> 3 , 1 /> 4 ]
  , [ 1 /> 1, 0 /> 1, 1 /> 3, 1 /> 3 , 1 /> 4 , 0 /> 4 , 0 /> 4 , 0 /> 5 ]
  , [ 0 /> 1, 0 /> 1, 1 /> 3, 1 /> 3 , 1 /> 4 , 0 /> 4 , 0 /> 4 , 0 /> 5 ]
  , [ 0 /> 2, 0 /> 2, 1 /> 3, 1 /> 3 , 1 /> 4 , 0 /> 5 , 0 /> 5 , 0 /> 6 ]
  ]

||| Reduce given unit by one step, updating its state
public export
reduce : (unit : GameUnit) -> (units : List (GameUnit, Pos)) -> List (GameUnit, Pos)
reduce unit = catMaybes . map (\ (u,p) => reduceUnit u p)
  where
    reduceUnit : GameUnit -> Pos -> Maybe (GameUnit, Pos)
    reduceUnit u@(MkGameUnit nation unitType name parent size move currentMP steps hits combat) pos =
      if u /= unit
      then Just (u, pos)
      else case strengthen (FS hits) of
             Left  _ => Nothing
             Right h => Just (MkGameUnit nation unitType name parent size move currentMP steps h combat, pos)

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import IsEven
import Matrix
import VecSort
import Vectors
import WordLength
import WordLength_vec
import XOR


text:
module Task.Internal

import public Control.Monad.Ref

import public Task.Universe
import public Task.Input

%default total
%access export

%hide Language.Reflection.Ref
%hide Language.Reflection.Universe

infix  6 =~, /~

-- Tasks -----------------------------------------------------------------------

public export
data TaskT : (m : Type -> Type) -> (r : Ty) -> Type where

  -- Core
  Edit  : (val : Maybe (typeOf r)) -> TaskT m r
  Store : MonadRef l m => l (typeOf r) -> TaskT m r

  -- Parallel
  And   : (left : TaskT m a) -> (right : TaskT m b) -> TaskT m (PAIR a b)

  -- Choice
  Or    : (left : TaskT m r) -> (right : TaskT m r) -> TaskT m r
  Xor   : (left : TaskT m r) -> (right : TaskT m r) -> TaskT m r
  Fail  : TaskT m r

  -- Sequence
  Then  : (this : TaskT m a) -> (next : typeOf a -> TaskT m r) -> TaskT m r
  Next  : (this : TaskT m a) -> (next : typeOf a -> TaskT m r) -> TaskT m r

  -- Labels
  Label : Label -> (this : TaskT m r) -> TaskT m r

  -- Lifts
  Lift  : Monad m => m (typeOf a) -> TaskT m a

-- Labels ----------------------------------------------------------------------

||| Get the current label, if one
label : TaskT m a -> Maybe Label
label (Label l _) = Just l
label _           = Nothing

||| Remove as much labels as possible from a task.
|||
||| Usefull to deeply match task constructors while ignoring labels.
delabel : TaskT m a -> TaskT m a
delabel (Label _ t) = delabel t
delabel t           = t

||| Match a label to a task.
(=~) : Label -> TaskT m a -> Bool
(=~) k (Label l _) = l == l
(=~) _ _           = False

||| Negation of `(=~)`.
(/~) : Label -> TaskT m a -> Bool
(/~) l t = not (l =~ t)

||| Collect all labels in an external choice
labels : TaskT m a -> List Label
labels (Label _ Fail)   = []
labels (Label l this)   = l :: labels this
labels (Xor left right) = labels left ++ labels right
-- --FIXME: should we also check for labels on the lhs of a step (see also `find`)?
-- labels (Then this _)    = labels this
-- labels (Next this _)    = labels this
labels _                = []

||| Depth first search for a label on a task tree.
|||
||| Returns the path of the found task.
find : Label -> TaskT m a -> Maybe Path
find k (Label l this) with ( k == l )
  | True                = Just GoHere
  | False               = find k this
find k (Xor left right) = map GoLeft (find k left) <|> map GoRight (find k right)
-- --FIXME: should we can send pick-events through to the lhs of a step (see also `labels`)?
-- find k (Then this _)    = find k this
-- find k (Next this _)    = find k this
find k _                = Nothing

||| Check if a task constructor keeps its label after stepping or loses it.
keeper : TaskT m a -> Bool
keeper (Edit _)  = True
keeper (And _ _) = True
keeper (Fail)    = True
keeper _         = False

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
> module BoundedNat.Properties

> import Data.Fin
> import Control.Isomorphism
> import Syntax.PreorderReasoning

> import BoundedNat.BoundedNat
> import BoundedNat.Operations
> import Basic.Operations
> import Nat.LTProperties
> import Sigma.Sigma
> import Pairs.Operations
> import Sigma.Properties
> import Fin.Properties
> import Finite.Predicates
> import Unique.Predicates

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

No natural number is smaller than zero

> implementation [UninhabitedLTBZ] Uninhabited (LTB Z) where
>   uninhabited (MkSigma n prf) = absurd prf

Basic properties

> |||
> toFinLemma0 : (n : Nat) -> (b : Nat) -> (prf : LT n b) ->
>               finToNat (toFin (MkSigma n prf)) = n
> toFinLemma0   n     Z             prf  = absurd prf
> toFinLemma0   Z    (S a) (LTESucc prf) = Refl
> toFinLemma0  (S m) (S a) (LTESucc prf) = let ih = toFinLemma0 m a prf
>                                          in rewrite ih in Refl
> %freeze toFinLemma0 -- frozen

> |||
> toFinLemma1 : (n : Nat) -> (b : Nat) -> (prf : LT n b) ->
>               finToNat (FS (toFin (MkSigma n prf))) = S n
> toFinLemma1 n b prf =
>     ( finToNat (FS (toFin (MkSigma n prf))) )
>   ={ Refl }=                             -- definition of |finToNat|
>     ( S (finToNat (toFin (MkSigma n prf)))  )
>   ={ cong (toFinLemma0 n b prf) }=       -- |toFinLemma0|, functionality of |S|
>     ( S n                              )
>   QED
> %freeze toFinLemma1 -- frozen

> |||
> toFinLemma2 : (n : Nat) -> (b : Nat) -> (prf : LT n b) ->
>               finToNatLemma (toFin (MkSigma n prf)) = prf
> toFinLemma2   n     Z     prf              = absurd prf
> toFinLemma2   Z    (S b) (LTESucc LTEZero) = Refl
> {-
> toFinLemma2  (S n) (S b) (LTESucc prf) =
>     ( finToNatLemma (toFin (S n ** LTESucc prf)) )
>   ={ Refl }=                                       -- definition of |toFin|
>     ( finToNatLemma (FS (toFin (n ** prf)))      )
>   ={ Refl }=                                       -- definition of |finToNatLemma|
>     ( LTESucc (finToNatLemma (toFin (n ** prf))) )
>   ={ depCong2' {alpha = Nat}
>                {P = \ n => LT n b}
>                {Q = \ n, prf => LT (S n) (S b)}
>                {a1 = finToNat (toFin (n ** prf))}
>                {a2 = n}
>                {Pa1 = finToNatLemma (toFin (n ** prf))}
>                {Pa2 = prf}
>                (\ n, prf => LTESucc prf)
>                (toFinLemma0 n b prf)
>                (toFinLemma2 n b prf) }=
>     ( LTESucc prf                                )
>   QED
> -}
> --{-
> toFinLemma2  (S n) (S b) (LTESucc prf) = trans s1 (trans s2 s3) where
>   s1 : finToNatLemma (toFin (MkSigma (S n) (LTESucc prf)))
>        =
>        finToNatLemma (FS (toFin (MkSigma n prf)))
>   s1 = Refl
>   s2 : finToNatLemma (FS (toFin (MkSigma n prf)))
>        =
>        LTESucc (finToNatLemma (toFin (MkSigma n prf)))
>   s2 = Refl
>   {-
>   sx : finToNatLemma (toFin (n ** prf))
>        =
>        prf
>   sx = toFinLemma2 n b prf
>   sy : LTESucc (finToNatLemma (toFin (n ** prf)))
>        =
>        LTESucc prf
>   sy = cong {a = finToNatLemma (toFin (n ** prf))} {b = prf} {f = LTESucc} sx
>   -}
>   s3 : LTESucc (finToNatLemma (toFin (MkSigma n prf)))
>        =
>        LTESucc prf
>   s3 = depCong2' {alpha = Nat}
>                  {P = \ n => LT n b}
>                  {Q = \ n, prf => LT (S n) (S b)}
>                  {a1 = finToNat (toFin (MkSigma n prf))}
>                  {a2 = n}
>                  {Pa1 = finToNatLemma (toFin (MkSigma n prf))}
>                  {Pa2 = prf}
>                  {f = \ n, prf => LTESucc prf}
>                  (toFinLemma0 n b prf)
>                  (toFinLemma2 n b prf)
> ---}
> %freeze toFinLemma2 -- frozen

> |||
> toFinLemma3 : (n : Nat) -> (b : Nat) -> (prf : LT n b) ->
>               finToNatLemma (FS (toFin (MkSigma n prf))) = LTESucc prf
> {-
> toFinLemma3 n b prf =
>     ( finToNatLemma (FS (toFin (n ** prf)))      )
>   ={ replace {a = Fin (S b)}
>              {x = FS (toFin (n ** prf))}
>              {y = toFin (S n ** LTESucc prf)}
>              {P = \ x => finToNatLemma (FS (toFin (n ** prf))) = finToNatLemma x}
>              Refl Refl }=
>     ( finToNatLemma (toFin (S n ** LTESucc prf)) )
>   ={ toFinLemma2 (S n) (S b) (LTESucc prf) }=
>     ( LTESucc prf                                )
> -}
> toFinLemma3 n b prf = trans s1 s2 where
>   s0 : FS (toFin (MkSigma n prf)) = toFin (MkSigma (S n) (LTESucc prf))
>   s0 = Refl
>   s1 : finToNatLemma (FS (toFin (MkSigma n prf)))
>        =
>        finToNatLemma (toFin (MkSigma (S n) (LTESucc prf)))
>   s1 = replace {a = Fin (S b)}
>                {x = FS (toFin (MkSigma n prf))}
>                {y = toFin (MkSigma (S n) (LTESucc prf))}
>                {P = \ x => finToNatLemma (FS (toFin (MkSigma n prf))) = finToNatLemma x}
>                s0 Refl
>   s2 : finToNatLemma (toFin (MkSigma (S n) (LTESucc prf)))
>        =
>        LTESucc prf
>   s2 = toFinLemma2 (S n) (S b) (LTESucc prf)
> %freeze toFinLemma3 -- frozen

> {-
> |||
> toFinLemma6 : (n : Nat) -> (b : Nat) -> (prf : LT n b) ->
>               toFin (S n ** LTESucc prf) = FS (toFin (n ** prf))
> -}

> ||| |toFin| is the left-inverse of |fromFin|
> toFinFromFinLemma : (k : Fin b) -> toFin (fromFin k) = k
> toFinFromFinLemma {b = Z} k = absurd k
> toFinFromFinLemma {b = S m} FZ = Refl
> toFinFromFinLemma {b = S m} (FS k) =
>   let ih = toFinFromFinLemma k in
>   rewrite ih in
>   Refl
> %freeze toFinFromFinLemma -- frozen

> using implementation UninhabitedLTBZ
>   ||| |fromFin| is the left-inverse of |toFin|
>   fromFinToFinLemma : (n : LTB b) -> fromFin (toFin n) = n
>   fromFinToFinLemma {b = Z}   k                                   = absurd k
>   fromFinToFinLemma {b = S m} (MkSigma   Z    (LTESucc LTEZero))  = Refl
>   fromFinToFinLemma {b = S m} (MkSigma (S n) (LTESucc prf))       = s6 where
>     s1 : fromFin (toFin (MkSigma (S n) (LTESucc prf)))
>          =
>          fromFin (FS (toFin (MkSigma n prf)))
>     s1 = Refl
>     s2 : fromFin (FS (toFin (MkSigma n prf)))
>          =
>          MkSigma (finToNat (FS (toFin (MkSigma n prf)))) (finToNatLemma (FS (toFin (MkSigma n prf))))
>     s2 = Refl
>     s3 : finToNat (FS (toFin (MkSigma n prf))) = S n
>     s3 = toFinLemma1 n m prf
>     s4 : finToNatLemma (FS (toFin (MkSigma n prf))) = LTESucc prf
>     s4 = toFinLemma3 n m prf
>     s5 : MkSigma {A = Nat} {P = \ i => LT i (S m)}
>          (finToNat (FS (toFin (MkSigma n prf))))
>          (finToNatLemma (FS (toFin (MkSigma n prf))))
>          =
>          MkSigma {A = Nat} {P = \ i => LT i (S m)} (S n) (LTESucc prf)
>     s5 = depCong2 {f = MkSigma {A = Nat} {P = \ i => LT i (S m)}} s3 s4
>     s6 : fromFin (toFin (MkSigma (S n) (LTESucc prf))) = MkSigma (S n) (LTESucc prf)
>     s6 = trans s1 (trans s2 s5)
>   %freeze fromFinToFinLemma

Finitness properties

> ||| Bounded |Nat|s are finite:
> finiteLTB : (b : Nat) -> Finite (LTB b)
> finiteLTB b = MkSigma b iso where
>   iso : Iso (LTB b) (Fin b)
>   iso = MkIso toFin fromFin toFinFromFinLemma fromFinToFinLemma
> %freeze finiteLTB -- frozen

> {-
> ||| Subtypes of bounded |Nat|s are finite:
> finiteSubLTB : (b : Nat) -> (P : LTB b -> Type) -> Dec1 P -> (uP : Unique1 P) -> Finite (SubType (LTB b) P uP)
> finiteSubLTB b P dP uP = finiteSubTypeLemma0 {A = LTB b} {P} (finiteLTB b) dP uP
> -}

Decidability properties

> ||| Equality of bounded |Nat|s is decidable
> decEqLTB : {b : Nat} -> (i : LTB b) -> (j : LTB b) -> Dec (i = j)
> decEqLTB {b} (MkSigma m p) (MkSigma n q) with (decEq m n)
>   | (Yes prf)   = Yes (sigmaEqLemma1 (MkSigma m p) (MkSigma n q) prf (uniqueLT))
>   | (No contra) = No (\ prf => contra (getWitnessPreservesEq prf))
> %freeze decEqLTB -- frozen

> implementation [DecEqLTB] DecEq (LTB b) where
>   decEq {b} i j = decEqLTB {b} i j

Show

> using (b : Nat)
>   implementation [ShowLTB] Show (LTB b) where
>     show (MkSigma i _) = show i

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
%default total

g3 : (Nat, Nat) -> Nat
g3 (x, y) = x
g3 _ = 6

f : Monad m => m (Nat, Nat)

h3 : Monad m => m Nat
h3 = do
  (x, y) <- f
    | _ => pure 5
  pure x


text:
module Poker.Deck

import Control.ST
import Control.ST.Random
import Data.Fin
import Data.Vect

%access public export
%default total

elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
elemSmallerThanBound FZ = LTESucc LTEZero
elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)

data Suit = Spade | Heart | Diamond | Club

DecEq Suit where
  decEq Spade Spade = Yes Refl
  decEq Spade Heart = No $ \Refl impossible
  decEq Spade Diamond = No $ \Refl impossible
  decEq Spade Club = No $ \Refl impossible
  decEq Heart Spade = No $ \Refl impossible
  decEq Heart Heart = Yes Refl
  decEq Heart Diamond = No $ \Refl impossible
  decEq Heart Club = No $ \Refl impossible
  decEq Diamond Spade = No $ \Refl impossible
  decEq Diamond Heart = No $ \Refl impossible
  decEq Diamond Diamond = Yes Refl
  decEq Diamond Club = No $ \Refl impossible
  decEq Club Spade = No $ \Refl impossible
  decEq Club Heart = No $ \Refl impossible
  decEq Club Diamond = No $ \Refl impossible
  decEq Club Club = Yes Refl

Rank : Type
Rank = Fin 13

record Card where
  constructor MkCard
  suit : Suit
  rank : Rank

enumFinHelp : (b : Nat) -> Vect a (Fin a) -> Vect (b + a) (Fin (b + a))
enumFinHelp Z xs = xs
enumFinHelp {a} (S k) xs =
  let  xs' = last :: map weaken xs
  in rewrite plusSuccRightSucc k a in
  enumFinHelp k xs'

enumFin : (n : Nat) -> Vect n (Fin n)
enumFin n =
  rewrite sym (plusZeroRightNeutral n) in
  enumFinHelp n []

outerBy : (a -> b -> c) -> Vect m a -> Vect n b -> Vect (m * n) c
outerBy {m} {n} f xs ys =
  concat {m = m} {n = n} $ map (\x => map (f x) ys) xs

suits : Vect 4 Suit
suits = [Spade, Heart, Diamond, Club]

ranks : Vect 13 Rank
ranks = enumFin 13

ace : Rank
ace = the Rank last

newDeck : Vect 52 Card
newDeck =
  let ss = suits
      rs = ranks
  in outerBy MkCard ss rs

data Cut : (m : Nat) -> Vect o t -> Type where
  MkCut : (f : Vect m t) ->
          (c : t) ->
          (b : Vect n t) ->
          Cut m (f ++ c :: b)

plusOnePlusSucc : (m : Nat) -> (i' : Nat) -> plus (plus m 1) i' = S (plus m i')
plusOnePlusSucc m i' = rewrite plusCommutative m 1 in Refl

cutHelp : (f : Vect m t ) ->
          (b : Vect (S n) t ) ->
          (i : Nat) ->
          (lt : LT i (S n)) ->
          Cut (m + i) (f ++ b)
cutHelp {m = m} {n = n} f (c :: b) Z lt =
  rewrite plusZeroRightNeutral m in
  MkCut f c b
cutHelp {m = m} {n = Z} f (c :: b) (S i') (LTESucc lt') = absurd lt'
cutHelp {m = m} {n = (S n')} f (c :: b) (S i') (LTESucc lt') =
  let rec = cutHelp (f ++ [c]) b i' lt'
  in rewrite vectAppendAssociative f [c] b in
     rewrite sym $ plusSuccRightSucc m i' in
     rewrite sym $ plusOnePlusSucc m i' in
     rec

cut : (i : Nat) -> (xs : Vect n t) ->
      {auto smaller : LT i n} ->
      Cut i xs
cut {n = Z} i xs {smaller = smaller} = absurd smaller
cut {n = (S k)} i xs {smaller = smaller} = cutHelp [] xs i smaller

data Shuffle : Vect n t -> Type where
  EmptyShuffle : (xs : Vect Z t) -> Shuffle xs
  Deal : (c : t) -> Shuffle (f ++ b) -> Shuffle (f ++ c :: b)

mutual
  shuffleHelp : (rnd : Var) -> (xs : Vect n t) ->
                (i : Fin n) ->
                ST m (Shuffle xs) [rnd ::: Random]
  shuffleHelp {t} rnd xs i with (elemSmallerThanBound i)
    shuffleHelp {t} rnd xs i | lt with (finToNat i)
      shuffleHelp {t} rnd xs i | lt | i' with (cut i' xs)
        shuffleHelp {t} rnd (f ++ c :: b) i | lt | i' | (MkCut f c b) = do
          rest <- shuffle rnd $ assert_smaller (f ++ c :: b) (f ++ b)
          pure (Deal {t = t} {f = f} {b = b} c rest)

  shuffle : (rnd : Var) -> (xs : Vect n t) -> ST m (Shuffle xs) [rnd ::: Random]
  shuffle {n = Z} rnd [] = pure (EmptyShuffle [])
  shuffle {n = (S n')} rnd xs = do
    i <- rndFin rnd n'
    shuffleHelp rnd xs i

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

max_stars_repo_name: farrellm/idris-poker

max_issues_repo_name: farrellm/idris-poker

max_forks_repo_name: farrellm/idris-poker


text:
module Main

import Data.Array16Spec
import Data.HashMapSpec

main : IO ()
main = do
    ignore $ specArray16
    ignore $ specHashMap


text:
module Turing

%default total

-- Re-implementation of 'Totality vs Turing Completeness' by Conor McBride
--

data General : (S: Type) -> (T: S -> Type) -> (X : Type) -> Type where
  Res   : x -> General s t x
  Req   : {S : Type} -> (s: S) -> (t s -> General S t x) -> General S t x

fold : {S : Type} -> (x -> y) -> ((s:S) -> (t s -> y) -> y) -> General S t x -> y
fold r c (Res x)     = r x
fold r c (s `Req` k) = c s (\t => fold r c (k t))

call : {S: Type} -> (s:S) -> General S t (t s)
call s = s `Req` Res

PiG : (S : Type) -> (T: S -> Type) -> Type
PiG S T = (s : S) -> General S T (T s)

halting : (s -> Bool) -> (s -> s) -> PiG s (const s)
halting stop step start with (stop start)
                         | True  = Res start
                         | False = call (step start)

-- namespace Kleisli
--   data Kleisli : -- {x: Type} -> {y: Type} ->
--                  {F: Type -> Type} -> {G: Type -> Type} ->
--                  (M : F i -> G j) -> Type where

max_stars_repo_name: braje/totality-talk

max_issues_repo_name: braje/totality-talk

max_forks_repo_name: braje/totality-talk


text:
-- DataStore.idr
--
-- A simple Vect-based data store with
-- integer key and string values

module Main

import Data.Vect

infix 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

||| A record-style DataStore type
record DataStore where
       constructor MkData
       schema : Schema
       size : Nat
       items : Vect size (SchemaType schema)

{-
addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newItem = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newItem]
    addToData (x :: xs) = x :: (addToData xs)

||| commands for data store
data Command = Add String
             | Get Integer
             | Search String
             | Size
             | Quit

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "search" str = Just (Search str)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

||| Parses given string and returns matching command
||| if sucessful (or Nothing in case of invalid string)
parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store in
                         case integerToFin pos (size store) of
                              Nothing => Just ("Out of range\n", store)
                              (Just id) => Just (index id store_items ++ "\n", store)

findEntriesString : (idx : Nat) -> (str : String) -> (items : Vect len String) -> String
findEntriesString idx str [] = "\n"
findEntriesString idx str (x :: xs) = if (isInfixOf str x)
                                         then (show idx) ++ ": " ++ x ++ "\n" ++ findEntriesString (idx + 1) str xs
                                         else findEntriesString (idx + 1) str xs

findEntries : (str : String) -> (store : DataStore) -> String
findEntries str store = findEntriesString Z str (items store)

concatStringVect : (p : Nat ** Vect p (Nat, String)) -> String
concatStringVect (Z ** []) = "\n"
concatStringVect (S x ** ((id, str) :: items)) = (show id) ++ ": " ++ str ++ "\n" ++ concatStringVect (x ** items)

||| Processes given String command
processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse input of
                                Nothing => Just ("Unknown command: " ++ input ++ "\n", store)
                                Just (Add item) =>
                                  Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
                                Just (Get pos) => getEntry pos store
                                Just (Search str) =>
                                  Just (findEntries str store, store)
                                Just Size =>
                                  Just ("Size: " ++ cast (size store) ++ "\n", store)
                                Just Quit => Nothing

-- entry point
main : IO ()
main = replWith (MkData 0 []) "Command: " processInput

-}

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Main

import API.Web.Console
import API.Web.HTML.Window
import IdrisScript
import Interfaces
import Scenes.Main.Scene

--step:
-- 1.:
  -- poll events
  -- handle events
-- 2. update model using action
-- 3. render
-- 4. recurse step

step : (Updatable ty, FrameRequest ty) => ty -> JS_IO ()
step scene = requestFrame scene step' where
  step' : (delta : Double) -> JS_IO ()
  step' delta = step !(update scene)
-- step scene = ?requestAnimationFrame step where
--   step : () -> JS_IO ()
--   step = ?pollEvents >>= update scene >>= ?render >>= step

main : JS_IO ()
main = case !defaultWindow of
  Nothing       => log "Couldn't get default window Object"
  (Just window) => case !(initSceneWith window) of
    Nothing      => log "Couldn't init main scene"
    (Just scene) => step scene


text:
module InsertionSort

import Data.Vect

Smaller : Nat -> Nat -> Nat
Smaller Z n = Z
Smaller  m Z = Z
Smaller  (S m) (S n) = (S (Smaller m n))

Min : (m: Nat) -> (n: Nat) -> Either (LTE m n) (LTE n m)
Min Z n = Left LTEZero
Min m Z = Right LTEZero
Min (S a) (S b) = case (Min a b) of
                       (Left l) => Left (LTESucc l)
                       (Right r) => Right (LTESucc r)

Insert: (k: Nat) -> (Vect n Nat) -> (Vect (S n) Nat)
Insert k [] = [k]
Insert k (x :: xs) = case (Min k x) of
                        (Left l) => ([k] ++ [x]) ++ xs
                        (Right r) => [x] ++ (Insert k xs)

Sort: (Vect n Nat) -> (Vect n Nat)
Sort [] = []
Sort (x :: xs) = Insert x (Sort xs)

VectMin: (n: Nat) -> (Vect n Nat) -> Nat
VectMin Z [] = Z
VectMin (S Z) [k] = k
VectMin (S (S len)) (x :: xs) = Smaller (VectMin (S len) xs) (x)

CheckSortedVect : (n: Nat) -> (Vect n Nat) -> Bool
CheckSortedVect Z [] = True
CheckSortedVect (S Z) [k] = True
CheckSortedVect (S (S n)) (x :: xs) = case (isLTE x (VectMin (S n) xs)) of
                                         (Yes prf) => (CheckSortedVect (S n) xs)
                                         (No contra) => False


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Abs num, Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul
    fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
    negate x = 0 - x
    (-) = Sub

Abs ty => Abs (Expr ty) where
    abs = Abs


text:
module Main

-- Vect is a typed list, the first type argument is the number of elements, the second is the type of them.
-- x -> y means 'given an x, yields a y'
-- x -> y -> z means 'given an x and a y, yields a z', something like BiFunction<X, Y, Z> in Java or (X, Y) => Z in Scala, etc.
-- Suggest operations for the following types:
--
-- 1) Vect n elem -> Vect n elem -- identity/id
-- 2) Vect n elem -> Vect (n * 2) elem -- append/(++)
-- 3) Vect (1 + n) elem -> Vect n elem -- remove first element
-- Assume Bounded n is a number between 0 and n - 1,
-- Bounded n -> Vect n elem -> elem -- get at index

-- Function calls don't need parentheses, e.g., sin x rather than sin(x).

-- Functions are pure, no observable side effects. Idris is strict by default.
-- Real programs are possible, similar to Java methods that return
-- ListenableFuture<>, we set up a chain of actions but never actually wait on a
-- ListenableFuture.
-- Idris' IO is similar to ListenableFuture but there is no way of waiting.
-- Sounds slow but it isn't. IO String ~= ListenableFuture<String>.

example_integer : Integer
example_integer = 6 + 8 * 11 -- 94

example_double : Double
example_double = 2.1 * 20

reversing_a_string : String
reversing_a_string = reverse "abcdefg"

appending_strings : String
appending_strings = "Hello" ++ " " ++ "World!"

-- At the REPL, begun by executing idris with no command line args:
-- Idris> :t 2 + 2
-- 2 + 2 : Integer -- not 4 : Integer, :t doesn't execute anything.

-- Idris> 2 + 2
-- 4 : Integer

-- Idris> :t Type
-- Type : Type 1 -- The type of simple types is Type 1, the type of Type 1 is
-- Type 2, etc., but we only ever need to write Type.

-- Example program, needs module Main which is at the top of this file.
-- idris Chapter1.idr
-- Idris> :exec

main : IO ()
main = putStrLn "Hello, Idris World!"

-- Or idris Chapter1.idr -o Hello
-- ./Hello

-- If we don't know what a value should be yet we can add a hole, e.g.:
-- main = putStrLn ?greeting
-- This will compile and give a warning, but can be executed.

-- Can use this to help understand more complex types, e.g., when we want to
-- putStrLn a Char instead of a String
-- main = putStrLn (?convert 'x')
-- Chapter1> :t convert
-- convert : Char -> String
-- can replace convert with cast.
-- main = putStrLn (cast 'x')

-- Types are values. x = Int is fine.

-- Calculating a type given a Boolean as a input:
-- StringOrInt is a function, the convention is to capitalize functions that
-- return Type.
StringOrInt : Bool -> Type
StringOrInt x = case x of
  True => Int
  False => String

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
  True -> 94
  False => "Ninety four"

valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
  True => cast val
  False => val

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground