text:
module Help

import Data.Config
import Data.String
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal

%default total

||| The Help string for Harmony.
export
help : (decorated : Bool) -> String
help decorated = """
harmony \{subcommand "<subcommand>"}

\{heading "Subcommands"}:
  \{subcommand "help"}
   - Print help
  \{subcommand "config"} {\{argument "<property>"}} [\{argument "value"}]
   - Get or set the value of a configuration property. Not all properties
     can be set and read via this subcommand.
     \{argument "properties"}: \{join ", " settableProps}.
  \{subcommand "sync"}
   - Synchronize local config with information from GitHub.
  \{subcommand "pr"}
   - Identify an existing PR or create a new one for the current branch.
  \{subcommand "contribute"}
   - Contribute to an open PR. Prints a URL. Prioritizes PRs you are
     requested to review but will also return other PRs.
  \{subcommand "reflect"}
   - Reflect on the current state of ones own PRs and review requests.
  \{subcommand "list"} {\{argument "<team-slug>"}}
   - List the members of the given GitHub Team.
  \{subcommand "graph"} {\{argument "<team-slug>"}}
   - Graph the relative review workload of the members of the given GitHub Team.
  \{subcommand "assign"} {\{argument "<team-slug>"} | \{argument "+<user-login>"}} [...]
   - Assign the given team(s) and one lucky member from one of those teams
     to review the PR for the current branch.

     Also assign any users with logins specified. You specify these
     additional users by prefixing their logins with '+'.

\{heading "Bash Completion"}:
  You can set up bash completion by adding the following to your resource
  or bash profile:

    \{shell "eval \"$(harmony --bash-completion-script)\""}

  Zsh users will also need to have the following in their resource or
  zsh profile before the above eval:

    \{shell "autoload -U +X compinit && compinit"}
    \{shell "autoload -U +X bashcompinit && bashcompinit"}

"""
  where
    maybeDecorate : (String -> Doc AnsiStyle) -> String -> String
    maybeDecorate f s = if decorated then renderString . layoutPretty defaultLayoutOptions $ f s else s

    subcommand : String -> String
    subcommand = maybeDecorate (annotate (color Magenta) . pretty)

    argument : String -> String
    argument = maybeDecorate (annotate (color Blue) . pretty)

    heading : String -> String
    heading = maybeDecorate (annotate underline . pretty)

    shell : String -> String
    shell = maybeDecorate (annotate italic . pretty)

ext: idr

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : UML.Class.Parser
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Class.Parser

import Lightyear
import Lightyear.Strings

import UML.Class.Model
import UML.Types

import UML.Utils.Parsing

%access private
-- -------------------------------------------------------------------- [ Misc ]
modifier : Parser Modifier
modifier = do token "static"
              pure Static
       <|> do token "abstract"
              pure Abstract
       <?> "Modifier"

visibility : Parser Visibility
visibility = do token "-"
                pure Private
         <|> do token "+"
                pure Public
         <|> do token "~"
                pure Package
         <|> do token "#"
                pure Protected
         <?> "Visibility"

-- ---------------------------------------------------------------- [ Relation ]
description : Parser String
description = do
    colon
    x <- literallyBetween '\"'
    pure x

relationType : Parser RelationTy
relationType = do token "<|--"
                  pure Specialisation
           <|> do token "o--"
                  pure Composition
           <|> do token "*--"
                  pure Aggregation
           <|> do token "<--"
                  pure Realisation
           <|> do token "-->"
                  pure Association
           <?> "Relation Type"

relation : Parser $ ClassModel RELA
relation = do
    f <- ident <* space
    relTy <- relationType
    t <- ident <* space
    desc <- opt description
    pure $ Relation relTy f t desc

-- ------------------------------------------------------------------ [ Params ]

param : Parser $ ClassModel PARAM
param = do
    id <- ident <* space
    colon
    ty <- ident <* space
    pure $ Param id ty
  <?> "Param"

params : Parser $ List $ ClassModel PARAM
params = sepBy1 param comma <?> "Params"

-- ----------------------------------------------------------------- [ Methods ]

method : Parser $ ClassModel METHOD
method = do
    mod <- opt $ braces modifier
    vis <- visibility
    id  <- ident
    ps  <- parens $ opt params
    colon
    ty <- ident
    pure $ Method id ty mod vis $ fromMaybe Nil ps
  <?> "Method"

-- -------------------------------------------------------------- [ Attributes ]

attribute : Parser $ ClassModel ATTR
attribute = do
    mod <- opt $ braces modifier
    vis <- visibility
    id  <- ident <* space
    colon
    ty  <- ident
    pure $ Attribute id ty mod vis
  <?> "Attribute"

-- ------------------------------------------------------------------- [ Class ]

classty : Parser ClassTy
classty = do token "Abstract"
             token "Class"
             return ClassAbstract
      <|> do token "Class"
             return ClassStandard
      <|> do token "Interface"
             return ClassInterface
      <?> "Class Type"

classDecl : Parser (ClassTy, String)
classDecl = do
    t <- classty
    i <- ident
    space
    pure (t,i)
  <?> "Class Delcaration"

emptyClass : Parser $ ClassModel CLASS
emptyClass = do
    (ty,id) <- classDecl
    let c = Clazz id ty Nil Nil
    pure c
  <?> "Empty Class"

element : Parser (Maybe $ ClassModel ATTR, Maybe $ ClassModel METHOD)
element = do a <- attribute
             eol
             pure (Just a, Nothing)
      <|> do m <- method
             eol
             pure (Nothing, Just m)
      <?> "Element"

classBody : Parser (List $ ClassModel ATTR, List $ ClassModel METHOD)
classBody = do
    es <- some element
    let (as', ms') = unzip es
    pure (catMaybes as', catMaybes ms')

bodyClass : Parser $ ClassModel CLASS
bodyClass = do
    (ty, id) <- classDecl
    (as, ms) <- braces classBody
    let c = Clazz id ty as ms
    pure c

clazz : Parser $ ClassModel CLASS
clazz = bodyClass <|> emptyClass <?> "Class"

-- ----------------------------------------------------------- [ Class Diagram ]

public
classModel : Parser UML
classModel = do
    cs <- some (clazz <* space)
    rs <- some (relation <* space)
    pure $ Class $ MkClassModel cs rs
  <?> "Class Diagram"
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Hoare

import Assn
import Expr
import Imp
import Logic
import Maps

%access public export

%default total

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

hoare_post_true : ((st : State) -> q st) -> HoareTriple p c q
hoare_post_true f _ st' _ _ = f st'

hoare_pre_false : ((st : State) -> Not (p st)) -> HoareTriple p c q
hoare_pre_false f = \st, st', rel, p_st => absurd $ f st p_st

hoare_assign : (q : Assertion) -> HoareTriple (AssignSub x a q) (x ::= a) q
hoare_assign q = \st, _, (E_Ass prf), q_st => rewrite sym prf in q_st

assn_sub_example : HoareTriple (AssignSub X (X + 1) (\st => LT (st X) 5))
                               (X ::= X + 1)
                               (\st => LT (st X) 5)
assn_sub_example = hoare_assign (\st => LT (st X) 5)

hoare_assign_fwd : (m : Nat) -> (a : AExp) -> (p : Assertion) ->
                   HoareTriple (\st => (p st, st X = m))
                               (X ::= a)
                               (\st => ( p (t_update X m st)
                                       , st X = aeval (t_update X m st) a ))
hoare_assign_fwd m a p st _ (E_Ass {n} prf1) (p_st, prf2) =
  rewrite sym prf2
  in rewrite trans (t_update_shadow {x=X} {v2=st X} {v1=n} {m=st})
                   (t_update_same {x=X} {m=st})
  in (p_st, sym prf1)

hoare_assign_fwd_exists : (a : AExp) -> (p : Assertion) ->
                          HoareTriple
                            (\st => p st)
                            (X ::= a)
                            (\st => (m ** ( p (t_update X m st)
                                          , st X = aeval (t_update X m st) a )))
hoare_assign_fwd_exists a p st st' rel p_st with (st X) proof prf2
  hoare_assign_fwd_exists a p st st' rel p_st | m =
    (m ** hoare_assign_fwd m a p st st' rel (p_st, sym prf2))

hoare_consequence_pre : (p, p', q : Assertion) -> HoareTriple p' c q ->
                        (p ->> p') -> HoareTriple p c q
hoare_consequence_pre p p' q ht imp = \st, st', rel, p_st =>
  ht st st' rel (imp st p_st)

hoare_consequence_post : (p, q, q' : Assertion) -> HoareTriple p c q' ->
                         (q' ->> q) -> HoareTriple p c q
hoare_consequence_post p q q' ht imp = \st, st', rel, p_st =>
  imp st' (ht st st' rel p_st)

hoare_assign_example_1 : HoareTriple (const ()) (X ::= 1) (\st => st X = 1)
hoare_assign_example_1 =
  hoare_consequence_post (const ())
                         (\st => st X = 1)
                         (\st => (m : Nat ** ((), st X = 1)))
                         (hoare_assign_fwd_exists 1 (const ()))
                         (\_, (_ ** (_, prf)) => prf)

hoare_assign_example_2 : HoareTriple (\st => LT (st X) 4)
                                     (X ::= X + 1)
                                     (\st => LT (st X) 5)
hoare_assign_example_2 =
  hoare_consequence_pre (\st => LT (st X) 4)
                        (\st => LT (st X + 1) 5)
                        (\st => LT (st X) 5)
                        (hoare_assign (\st => LT (st X) 5))
                        (\st, p_st => replace {P=\x => LT x 5}
                                              (sym (plusCommutative (st X) 1))
                                              (LTESucc p_st))

hoare_consequence : (p, p', q, q' : Assertion) -> HoareTriple p' c q' ->
                    p ->> p' -> q' ->> q -> HoareTriple p c q
hoare_consequence p p' q q' ht p_imp_p' q'_imp_q =
  let ht' = hoare_consequence_pre p p' q' ht p_imp_p'
  in hoare_consequence_post p q q' ht' q'_imp_q

hoare_assign_example_5 : HoareTriple (\st => LTE (st X + 1) 5)
                                     (X ::= X + 1)
                                     (\st => LTE (st X) 5)
hoare_assign_example_5 = hoare_assign (\st => LTE (st X) 5)

hoare_assign_example_6 : HoareTriple (\st => (LTE 0 3, LTE 3 5))
                                     (X ::= 3)
                                     (\st => (LTE 0 (st X), LTE (st X) 5))
hoare_assign_example_6 = hoare_assign (\st => (LTE 0 (st X), LTE (st X) 5))

hoare_skip : (p : Assertion) -> HoareTriple p SKIP p
hoare_skip _ _ _ E_Skip p_st = p_st

hoare_seq : (p, q, r : Assertion) -> HoareTriple q c2 r -> HoareTriple p c1 q ->
            HoareTriple p (do c1; c2) r
hoare_seq p q r ht2 ht1 = \st, st', (E_Seq {st2} cc1 cc2), p_st =>
  let q_st2 = ht1 st st2 cc1 p_st
  in ht2 st2 st' cc2 q_st2

hoare_assign_example_3 : (a : AExp) -> (n : Nat) ->
                         HoareTriple (\st => aeval st a = n)
                                     (do X ::= a; SKIP)
                                     (\st => st X = n)
hoare_assign_example_3 a n =
  let hta = hoare_assign_fwd_exists a (\st => aeval st a = n)
      hta' = hoare_consequence_post
               (\st => aeval st a = n)
               (\st => st X = n)
               (\st => (m : Nat ** ( aeval (t_update X m st) a = n
                                   , st X = aeval (t_update X m st) a )))
               hta
               (\_, (_ ** (aeval_eq_n, st_X_eq_aeval)) =>
                  trans st_X_eq_aeval aeval_eq_n)
      hts = hoare_skip (\st => st X = n)
  in hoare_seq (\st => aeval st a = n) (\st => st X = n) (\st => st X = n)
               hts hta'

hoare_assign_example_4 : HoareTriple (const ())
                                     (do X ::= 1; Y ::= 2)
                                     (\st => (st X = 1, st Y = 2))
hoare_assign_example_4 =
  let htx = hoare_consequence_post
              (const ())
              (\st => st X = 1)
              (\st => (m : Nat ** ((), st X = 1)))
              (hoare_assign_fwd_exists 1 (const ()))
              (\_, (_ ** (_, q_st)) => q_st)
      hty = hoare_consequence_pre
              (\st => st X = 1)
              (AssignSub Y 2 (\st => (st X = 1, st Y = 2)))
              (\st => (st X = 1, st Y = 2))
              (hoare_assign (\st => (st X = 1, st Y = 2)))
              (\_, p_st => (p_st, Refl))
  in hoare_seq (const ()) (\st => st X = 1) (\st => (st X = 1, st Y = 2))
               hty htx

swap_program : Com
swap_program = do Z ::= X
                  X ::= Y
                  Y ::= Z

swap_exercise : HoareTriple (\st => LTE (st X) (st Y))
                            Hoare.swap_program
                            (\st => LTE (st Y) (st X))
swap_exercise =
  let htz = hoare_consequence_pre
              (\st => LTE (st X) (st Y))
              (AssignSub Z X (\st => LTE (st Z) (st Y)))
              (\st => LTE (st Z) (st Y))
              (hoare_assign (\st => LTE (st Z) (st Y)))
              (\_, p_st => p_st)
      htx = hoare_consequence_pre (\st => LTE (st Z) (st Y))
                                  (AssignSub X Y (\st => LTE (st Z) (st X)))
                                  (\st => LTE (st Z) (st X))
                                  (hoare_assign (\st => LTE (st Z) (st X)))
                                  (\_, p_st => p_st)
      hty = hoare_consequence_pre (\st => LTE (st Z) (st X))
                                  (AssignSub Y Z (\st => LTE (st Y) (st X)))
                                  (\st => LTE (st Y) (st X))
                                  (hoare_assign (\st => LTE (st Y) (st X)))
                                  (\_, p_st => p_st)
      htxy = hoare_seq (\st => LTE (st Z) (st Y))
                       (\st => LTE (st Z) (st X))
                       (\st => LTE (st Y) (st X))
                       hty
                       htx
  in hoare_seq (\st => LTE (st X) (st Y))
               (\st => LTE (st Z) (st Y))
               (\st => LTE (st Y) (st X))
               htxy
               htz

hoare_if : (p, q : Assertion) ->
           HoareTriple (\st => (p st, BAssn b st)) c1 q ->
           HoareTriple (\st => (p st, Not (BAssn b st))) c2 q ->
           HoareTriple p (CIf b c1 c2) q
hoare_if p q ht1 ht2 = \st, st', rel, p_st => case rel of
  E_IfTrue prf cc1 => ht1 st st' cc1 (p_st, prf)
  E_IfFalse prf cc2 => ht2 st st' cc2 (p_st, bexp_eval_false prf)

if_example : HoareTriple (const ())
                         (CIf (X == 0) (Y ::= 2) (Y ::= X + 1))
                         (\st => LTE (st X) (st Y))
if_example =
  let htt = hoare_consequence
              (\st => ((), BAssn (X == 0) st))
              (AssignSub Y 2 (\st => (LTE (st X) (st Y), BAssn (X == 0) st)))
              (\st => LTE (st X) (st Y))
              (\st => (LTE (st X) (st Y), BAssn (X == 0) st))
              (hoare_assign (\st => (LTE (st X) (st Y), BAssn (X == 0) st)))
              (\st, (_, p_st) => ( replace {P=\x => LTE x 2}
                                           (sym (fst (nat_beq_iff (st X) 0)
                                                p_st))
                                           LTEZero
                                 , p_st ))
              (\_, (q_st, _) => q_st)
      htf = hoare_consequence
              (\st => ((), Not (BAssn (X == 0) st)))
              (AssignSub Y (X + 1) (\st => ( LTE (st X) (st Y)
                                           , Not (BAssn (X == 0) st) )))
              (\st => LTE (st X) (st Y))
              (\st => (LTE (st X) (st Y), Not (BAssn (X == 0) st)))
              (hoare_assign (\st => ( LTE (st X) (st Y)
                                      , Not (BAssn (X == 0) st) )))
              (\st, (_, p_st) => (lteAddRight (st X), p_st))
              (\_, (q_st, _) => q_st)
  in hoare_if (const ()) (\st => LTE (st X) (st Y)) htt htf

if_minus_plus : HoareTriple (const ())
                            (CIf (X <= Y) (Z ::= Y - X) (Y ::= X + Z))
                            (\st => st Y = st X + st Z)
if_minus_plus =
  let htt = hoare_consequence
              (\st => ((), BAssn (X <= Y) st))
              (AssignSub Z (Y - X) (\st => ( st Y = st X + st Z
                                           , BAssn (X <= Y) st )))
              (\st => st Y = st X + st Z)
              (\st => (st Y = st X + st Z, BAssn (X <= Y) st))
              (hoare_assign (\st => (st Y = st X + st Z, BAssn (X <= Y) st)))
              (\st, (_, p_st) =>
                 ( sym (lte_plus_minus (fst (lte_beq_iff (st X) (st Y)) p_st))
                 , p_st ))
              (\_, (q_st, _) => q_st)
      htf = hoare_consequence_pre
              (\st => ((), Not (BAssn (X <= Y) st)))
              (AssignSub Y (X + Z) (\st => st Y = st X + st Z))
              (\st => st Y = st X + st Z)
              (hoare_assign (\st => st Y = st X + st Z))
              (\_, _ => Refl)
  in hoare_if (const ()) (\st => st Y = st X + st Z) htt htf

hoare_while : {b : BExp} -> {c : Com} -> (p : Assertion) ->
              HoareTriple (\st => (p st, BAssn b st)) c p ->
              HoareTriple p (WHILE b c) (\st => (p st, Not (BAssn b st)))
hoare_while {b} {c} p ht st _ (E_WhileEnd prf) p_st =
  (p_st, snd not_true_iff_false prf)
hoare_while {b} {c} p ht st st' (E_WhileLoop {st1} prf cbody cnext) p_st =
  hoare_while p ht st1 st' cnext (ht st st1 cbody (p_st, prf))

while_example : HoareTriple (\st => LTE (st X) 3)
                            (CWhile (X <= 2) (X ::= X + 1))
                            (\st => st X = 3)
while_example st st' rel lte_prf =
  let htc =  hoare_assign (\st => LTE (st X) 3)
      htc' = hoare_consequence_pre
               (\st => (LTE (st X) 3, beval st (X <= 2) = True))
               (\st => LTE (st X + 1) 3)
               (\st => LTE (st X) 3)
               htc
               (\st, p_st => replace {P=\x => LTE x 3}
                                     (sym (plusCommutative (st X) 1))
                                     (LTESucc (fst (lte_beq_iff (st X) 2)
                                                   (snd p_st))))
      htw = hoare_while (\st => LTE (st X) 3) htc'
      (below, contra) = htw st st' rel lte_prf
  in bounded__eq below (fst (lte_nbeq_iff (st' X) 2)
                            (fst not_true_iff_false contra))

always_loop_hoare : (p, q : Assertion) -> HoareTriple p (WHILE BTrue SKIP) q
always_loop_hoare p q =
  let htc = hoare_consequence_pre
              (\st => (p st, BAssn BTrue st))
              p
              p
              (hoare_skip p)
              (\st, (p_st, _) => p_st)
      htw = hoare_while p htc
  in hoare_consequence_post
           p
           q
           (\st => (p st, Not (BAssn BTrue st)))
           htw
           (\st, (_, contra) => absurd (contra Refl))

hoare_if1 : {b : BExp} -> {c : Com} -> (p, q : Assertion) ->
            HoareTriple (\st => (p st, BAssn b st)) c q ->
            (\st => (p st, Not (BAssn b st))) ->> q ->
            HoareTriple p (CIf1 b c) q
hoare_if1 {b} {c} p q htc _ st st' (E_If1True prf cc) p_st =
  htc st st' cc (p_st, prf)
hoare_if1 {b} {c} p q _ imp st _ (E_If1False prf) p_st =
  imp st (p_st, snd not_true_iff_false prf)

hoare_if1_good : HoareTriple (\st => st X + st Y = st Z)
                             (IF1 not (Y == 0) THEN
                                  X ::= X + Y
                              FI)
                             (\st => st X = st Z)
hoare_if1_good =
  let htc = hoare_consequence
              (\st => (st X + st Y = st Z, not (st Y == 0) = True))
              (AssignSub X (X + Y)
                         (\st => (st X = st Z, not (st Y == 0) = True)))
              (\st => st X = st Z)
              (\st => (st X = st Z, not (st Y == 0) = True))
              (hoare_assign (\st => (st X = st Z, not (st Y == 0) = True)))
              (\_, p_st => p_st)
              (\st, (q_st, _) => q_st)
      hts = hoare_consequence
              (\st => (st X + st Y = st Z, Not (not (st Y == 0) = True)))
              (\st => (st X = st Z, Not (not (st Y == 0) = True)))
              (\st => st X = st Z)
              (\st => (st X = st Z, Not (not (st Y == 0) = True)))
              (hoare_skip (\st => (st X = st Z, Not (not (st Y == 0) = True))))
              (\st, (plus_st_X_st_Y__st_Z, prf) =>
                  let st_Y_eq_0 = fst (nat_beq_iff (st Y) 0)
                                      (trans (sym (notInvolutive (st Y == 0)))
                                             (cong {f=not}
                                                   (fst not_true_iff_false prf)))
                      pf = trans (sym (plusZeroRightNeutral (st X)))
                                 (replace {P=\x => st X + x = st Z}
                                          st_Y_eq_0 plus_st_X_st_Y__st_Z)
                  in (pf, prf))
              (\st, (q_st, _) => q_st)
      imp = \st, (plus_st_X_st_Y__st_Z, prf) =>
        let st_Y_eq_0 = fst (nat_beq_iff (st Y) 0)
                            (trans (sym (notInvolutive (st Y == 0)))
                                   (cong {f=not} (fst not_true_iff_false prf)))
        in trans (sym (plusZeroRightNeutral (st X)))
                 (replace {P=\x => st X + x = st Z}
                          st_Y_eq_0 plus_st_X_st_Y__st_Z)
  in hoare_if1 (\st => st X + st Y = st Z) (\st => st X = st Z) htc imp

hoare_for : {init, updt, body : Com} -> {cond : BExp} -> (p, q : Assertion) ->
            HoareTriple p init q ->
            HoareTriple (\st => (q st, BAssn cond st)) (do body; updt) q ->
            HoareTriple p
                        (CFor init cond updt body)
                        (\st => (q st, Not (BAssn cond st)))
hoare_for {init} {updt} {body} {cond} p q ht_init ht_body_updt st st'
          (E_For ci (E_WhileEnd prf)) p_st =
  (ht_init st st' ci p_st, bexp_eval_false prf)
hoare_for {init} {updt} {body} {cond} p q ht_init ht_body_updt st st'
          (E_For ci {st2} (E_WhileLoop {st1} prf cb cn)) p_st =
  let q_st2 = ht_init st st2 ci p_st
      q_st1 = ht_body_updt st2 st1 cb (q_st2, prf)
  in hoare_while q ht_body_updt st1 st' cn q_st1

hoare_repeat : {c : Com} -> {b : BExp} -> (p, q : Assertion) ->
               HoareTriple p c q -> (\st => (q st, Not (BAssn b st))) ->> p ->
               HoareTriple p (CRepeat c b) (\st => (q st, BAssn b st))
hoare_repeat {c} {b} p q htc imp st st' (E_Repeat cc (E_WhileEnd prf)) p_st =
  let q_st' = htc st st' cc p_st
      btrue = trans (sym (notInvolutive (beval st' b))) (cong {f=not} prf)
  in (q_st', btrue)
hoare_repeat {c} {b} p q htc imp st st'
             r@(E_Repeat {st1} cc1 (E_WhileLoop prf cc2 cnext)) p_st =
  let q_st1 = htc st st1 cc1 p_st
      bfalse = bexp_eval_false (trans (sym (notInvolutive (beval st1 b)))
                                      (cong {f=not} prf))
      p_st1 = imp st1 (q_st1, bfalse)
  in hoare_repeat p q htc imp st1 st'
                  (assert_smaller r (E_Repeat cc2 cnext)) p_st1

hoare_repeat_good : HoareTriple (\st => LT 0 (st X))
                                (REPEAT do
                                   Y ::= X
                                   X ::= X - 1
                                 UNTIL X == 0 END)
                                (\st => (st X = 0, LT 0 (st Y)))
hoare_repeat_good =
  let hty = hoare_assign (\st => LT 0 (st Y))
      htx = hoare_assign (\st => LT 0 (st Y))
      htc = hoare_seq (\st => LT 0 (st X))
                      (\st => LT 0 (st Y))
                      (\st => LT 0 (st Y))
                      htx
                      hty
      ht_repeat = hoare_repeat
                    (\st => LT 0 (st X))
                    (\st => LT 0 (st Y))
                    htc
                    (\st, (_, prf) =>
                        notZeroImpliesGTZero
                          (fst (nat_nbeq_iff (st X) 0)
                          (fst not_true_iff_false prf)))
  in hoare_consequence_post (\st => LT 0 (st X))
                            (\st => (st X = 0, LT 0 (st Y)))
                            (\st => (LT 0 (st Y), BAssn (X == 0) st))
                            ht_repeat
                            (\st, (lte_prf, prf) =>
                              let pf = fst (nat_beq_iff (st X) 0) prf
                              in (pf, lte_prf))


text:
module Main

mutual
  %inline
  is_even : Int -> Int
  is_even n =
      if n == 0 then 1 else is_odd $ n-1

  is_odd : Int -> Int
  is_odd n =
      if n == 0 then 0 else is_even $ n-1

main : JS_IO ()
main = do
  putStr' $ show $ is_even 100001

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Ifui.Html

import Ifui.XDom
import Ifui.Dom

hDom : ADom DomNode
hDom =
  MkADom
    createElement
    appendChild
    replaceWith
    setTextContent
    setAttr
    addTargetValueEventListener
    addEmptyEventListener
    removeNode
  where
    setAttr : DomNode -> String -> String -> IO ()
    setAttr n k v =
      if k == "value" then setValue n v
                      else setAttribute n k v
    createChild : DomNode -> String -> IO DomNode
    createChild n tag =
      do
        c <- createElement tag
        appendChild n c
        pure c
    addTargetValueEventListener : DomNode -> String -> (String -> IO ()) -> IO (IO ())
    addTargetValueEventListener n x f =
      addEventListener x (\w => targetValue w >>= f) n
    addEmptyEventListener : DomNode -> String -> IO () -> IO (IO ())
    addEmptyEventListener n x f =
      addEventListener x (\_ => f) n

export
data HtmlAttribute : Type -> Type where
  MkHtmlAttribute : Attribute a -> HtmlAttribute a

export
data Html : Type -> Type where
  MkHtml : Xml a -> Html a

removeHtmlAttributeConstructor : HtmlAttribute a -> Attribute a
removeHtmlAttributeConstructor (MkHtmlAttribute x) = x

export
startHtmlView : {f : s -> Type} ->  s -> ((x:s) -> f x -> s) -> ((x : s) -> Html (f x)) -> IO ()
startHtmlView s update view =
  do
    node <- startView hDom s update (\x => let MkHtml z = view x in z)
    appendChild !body node

export
textSpan : String -> Html a
textSpan s = MkHtml $ XNode "span" [] (Left s)

export
input : List (HtmlAttribute a) -> Html a
input attributes = MkHtml $ XNode "input" (map removeHtmlAttributeConstructor attributes) (Right [])

max_stars_repo_name: rbarreiro/ifui

max_issues_repo_name: rbarreiro/ifui

max_forks_repo_name: rbarreiro/ifui


text:
module ArithSeq

%access export
%default total

namespace Preloaded

  %access public export
  %default total

  arithSum : Nat -> Nat
  arithSum Z = Z
  arithSum (S n) = S n + arithSum n

  -- We define our own function for dividing a natural
  -- number by 2.
  -- The existing Idris function divNatNZ
  -- is not a good choice because it is impossible (correct
  -- me if I my wrong) to prove many useful properties of
  -- divNatNZ.
  half : Nat -> Nat
  half (S (S n)) = S (half n)
  half _ = Z

  arithFormula : Nat -> Nat
  arithFormula n = half $ n * (n + 1)

lemma_half_puts_out : (k, x : Nat) -> half (k + (k + x)) = k + half x
lemma_half_puts_out Z     x = Refl
lemma_half_puts_out (S k) x = rewrite sym $ plusSuccRightSucc k (k + x) in
                              rewrite lemma_half_puts_out k x in
                              Refl

arithEq : (n : Nat) -> arithFormula n = arithSum n
arithEq Z     = Refl
arithEq (S k) = rewrite plusCommutative k 1 in
                rewrite multCommutative k (S (S k)) in
                rewrite lemma_half_puts_out k (k + k*k) in
                rewrite multCommutative (S k) k in
                rewrite plusCommutative 1 k in
                rewrite arithEq k in
                Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Control.Eff.Internal

import public Control.MonadRec
import public Control.Monad.Free
import public Data.Union

%default total

||| An effectful computation yielding a value
||| of type `t` and supporting the effects listed
||| in `fs`.
public export
Eff : (fs : List (Type -> Type)) -> (t : Type) -> Type
Eff fs t = Free (Union fs) t

||| Lift a an effectful comutation into the `Eff` monad.
export
send : Has f fs => f t -> Eff fs t
send = lift . inj

||| Handle all effectful computations in `m`,
||| returning the underlying free monad.
export
toFree : Eff fs t -> Handler fs m -> Free m t
toFree eff h = mapK (handleAll h) eff

||| Run an effectful computation without overflowing
||| the stack by handling all computations in monad `m`.
export
runEff : MonadRec m => Eff fs t -> Handler fs m -> m t
runEff eff h = foldMap (handleAll h) eff

||| Extract the (pure) result of an effectful computation
||| where all effects have been handled.
export
extract : Eff [] a -> a
extract fr = case toView fr of
  Pure val => val
  Bind u _ => absurd u

export
handleRelay :  (prf : Has f fs)
            => (a -> Eff (fs - f) b)
            -> (forall v . f v -> (v -> Eff (fs - f) b) -> Eff (fs - f) b)
            -> Eff fs a
            -> Eff (fs - f) b
handleRelay fval fcont fr = case toView fr of
  Pure val => fval val
  Bind x g => case decomp {prf} x of
    Left y  => assert_total $ lift y >>= handleRelay fval fcont . g
    Right y => assert_total $ fcont y (handleRelay fval fcont . g)

export
handleRelayS :  (prf : Has f fs)
             => s
             -> (s -> a -> Eff (fs - f) b)
             -> (forall v . s -> f v -> (s -> v -> Eff (fs - f) b) -> Eff (fs - f) b)
             -> Eff fs a
             -> Eff (fs - f) b
handleRelayS vs fval fcont fr = case toView fr of
  Pure val => fval vs val
  Bind x g => case decomp {prf} x of
    Left y  => assert_total $ lift y >>= handleRelayS vs fval fcont . g
    Right y => assert_total $ fcont vs y (\vs2 => handleRelayS vs2 fval fcont . g)


text:
module Functions

intFunction : Int
intFunction = 1887

stringFunction : String
stringFunction = "hello"

max_stars_repo_name: dkandalov/katas

max_issues_repo_name: dkandalov/katas

max_forks_repo_name: dkandalov/katas


text:
module Flutter.Widgets.Stateless

import Dart.FFI.Elab
import Flutter.FFI

%language ElabReflection

%inline
public export
Stateless : Type
Stateless = Struct """
_Stateless,
import 'package:flutter/material.dart' as material;

class _Stateless extends material.StatelessWidget {
  final material.Widget Function(material.BuildContext) onBuild;
  const _Stateless({material.Key key, this.onBuild}) : super(key: key);
  @$.override
  material.Widget build(material.BuildContext context) {
    return onBuild(context);
  }
}
""" []

%runElab importDart [
  package "" [
    partial' $
      class' "Stateless" [
        extends "Widget",
        const $ new "" [
          "key" :? "Key",
          "onBuild" :? "BuildContext" :-> "IO" :<> "Widget"
        ]
      ]
  ]
]


text:
%hide Prelude.integerToNat

data MyNat : Type where
    Z : MyNat
    S : MyNat -> MyNat

%builtin Natural MyNat

integerToMyNat : Integer -> MyNat
integerToMyNat i = if i <= 0
    then Z
    else S $ integerToMyNat (i - 1)

%builtin IntegerToNatural integerToMyNat

natToMyNat : Nat -> MyNat
natToMyNat Z = Z
natToMyNat (S k) = S $ natToMyNat k

%builtin IntegerToNatural natToMyNat

integerToNotNat : Integer -> Maybe String
integerToNotNat x = Just "Boo"

%builtin IntegerToNatural integerToNotNat


text:
module Lambdapants.Term.Nats

import Lambdapants.Term

%default total

||| Return the Church encoded term corresponding to the provided number.
export
encoded : Nat -> Term
encoded n = Lam "f" (Lam "x" nat) where
  nat : Term
  nat = foldr apply (Var "x") (replicate n (Term.App (Var "f")))

apps : String -> String -> Term -> Maybe Nat
apps f x = count 1 where
  count : Nat -> Term -> Maybe Nat
  count n (App (Var g) (Var v)) = if g == f && v == x then Just n else Nothing
  count n (App (Var g) e)       = if g == f then count (succ n) e else Nothing
  count _ _                     = Nothing

||| Return the natural number interpretation of the term, if it corresponds to
||| a valid Church encoding.
export
decoded : Term -> Maybe Nat
decoded (Lam f (Lam x term)) =
  case term of
       Var v   => if v == x then Just 0 else Nothing
       App _ _ => apps f x term
       Lam _ _ => Nothing
decoded _ = Nothing

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
module Network.ST.TcpSockets

import Control.ST
import Network.Socket

public export data TcpSocketState = Ready | Bound | Listening | Connected | Failed

Eq TcpSocketState where
  Ready == Ready = True
  Bound == Bound = True
  Listening == Listening = True
  Connected == Connected = True
  Failed == Failed = True
  _ == _ = False

public export addFirstIfJust : Type -> Action (Maybe (Var, a))
addFirstIfJust ty = Add (
  \inp => case inp of
    Nothing => []
    Just (v, _) => [v ::: ty]
                        )

public export
%error_reduce -- always evaluate this before showing errors
wrappedMaybeCaseOnly : {a : Type} -> {b : Type} -> {c : Type} -> (b -> c) -> b -> b -> Maybe a -> c
wrappedMaybeCaseOnly f x y m = f (if isJust m then y else x)

public export isConnectedOrFailedState : TcpSocketState -> Bool
isConnectedOrFailedState Connected = True
isConnectedOrFailedState Failed = True
isConnectedOrFailedState _ = False

-- Interface built using record not interface so we can use Sock more
-- easily.
public export record TcpSockets (m : Type -> Type) where
  constructor MkTcpSockets
  Sock : TcpSocketState -> Type
  -- A socket which is connected or failed, and which stores its state at runtime
  CFSock : Type
  socket : ST m (Either Int Var) [addIfRight $ Sock Ready]
  bind : (bindAddr: Maybe SocketAddress)
         -> (port : Int)
         -> (sock : Var)
         -> ST m Bool [sock ::: Sock Ready :-> (\v => if v then Sock Bound else Sock Ready)]
  listen : (sock : Var) -> ST m Bool [sock ::: Sock Bound :-> (\v => if v then Sock Listening else Sock Failed)]
  accept : (listeningSocket : Var)
           -> (withNewSocket : (newAddr: SocketAddress) -> (newSocket : Var)
                -> ST m () [remove newSocket (Sock Connected)])
           -> ST m (Maybe SocketAddress) [
                listeningSocket ::: Sock Listening :-> wrappedMaybeCaseOnly Sock Failed Listening
              ]
  close : {origSt : TcpSocketState} -> (sock : Var) -> ST m () [remove sock (Sock origSt)]
  readSocket : (sock : Var) -> ST m (Maybe String) [
    sock ::: Sock Connected :-> wrappedMaybeCaseOnly Sock Failed Connected
  ]
  writeSocket : (out : String) -> (sock : Var) -> ST m (Maybe String) [
    sock ::: Sock Connected :-> wrappedMaybeCaseOnly Sock Failed Connected
  ]
  toCFSock : (st : TcpSocketState) -> (prf: isConnectedOrFailedState st = True)
          -> (oldSock : Var)
          -> ST m () [oldSock ::: (Sock st) :-> CFSock]
  fromCFSock : (cfSock : Var) -> ST m Bool [
    cfSock ::: CFSock :-> (\v => Sock (if (v) then Connected else Failed))
  ]

-- Hardcoded for now - if not, we need to prove it is within bound and non-negative
readBufSize : ByteLength
readBufSize = 4096

%hint export ioTcpSockets : TcpSockets IO
ioTcpSockets = MkTcpSockets
  {- Sock -} (const $ State Socket)
  {- CFSock -} (State (Socket, Bool))
  {- socket -} (do
    Right rawSocket <- lift $ Socket.socket AF_INET6 Stream 0
      | Left err => pure (Left err)
    lbl <- new rawSocket
    pure (Right lbl))
  {- bind -} (\addr => \port => \sockVar => do
    resultCode <- (lift $ Socket.bind !(read sockVar) addr port)
    if resultCode == 0 then
      pure True
    else
      pure False)
  {- listen -} (\sockVar => do
    resultCode <- lift $ Socket.listen !(read sockVar)
    if resultCode == 0 then
      pure True
    else
      pure False)
  {- accept -} (\listeningSockVar => \withNewSocket => with ST do
    Right (newSock, addr) <- lift $ Socket.accept !(read listeningSockVar)
     | Left _ => pure Nothing
    call $ forkST $ with ST do
      newSockVar <- new newSock
      withNewSocket addr newSockVar
    pure $ Just addr)
  {- close -} (\sockVar => do
    lift $ Socket.close !(read sockVar)
    delete sockVar)
  {- readSocket -} (\sockVar => with ST do
      Right (resp, _) <- lift $ Socket.recv !(read sockVar) readBufSize
       | Left _ => pure Nothing
      pure (Just resp))
  {- writeSocket -} (\out => \sockVar => with ST do
      Right count <- lift $ Socket.send !(read sockVar) out
       | Left _ => pure Nothing
      let countNat : Nat = cast count

      -- Here we assert that any successful (non-negative) return value from
      -- send is less than or equal to the original size of the buffer. The manpage
      -- for send says:
      --   On success, these calls return the number of bytes sent.
      --   On error, -1 is returned, and errno is set appropriately.
      -- For this assertion to be falsified, the kernel would need to be telling us
      -- it had sent more data than we asked it to, which is against the contract
      -- of send.
      let sendReturnValueLTELength : LTE countNat (length out) = believe_me ()
      pure $ Just $ substr countNat ((length out) - countNat) out
    )
  {- toCFSock -} (\st, prf, sock => with ST do
    update sock $ \rawSock => (rawSock, if st == Connected then True else False)
  )
  {- fromCFSock -} (\cfSock => with ST do
    (rawSock, isConnected) <- read cfSock
    write cfSock rawSock
    pure isConnected
  )
  where
  forkIO : IO () -> IO ()
  forkIO f = do
    fork f
    pure ()
  forkST : ST IO () [] -> ST IO () []
  forkST = ST.lift . forkIO . ST.run


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

data Elem : a -> Vect n a -> Type where
     Here : Elem x (x :: xs)
     There : {xs : Vect n a} -> Elem x xs -> Elem x (y :: xs)

getIndex : Elem x xs -> Nat
getIndex Here = 0
getIndex (There p) = S (getIndex p)

Beatles : Vect ? String
Beatles = ["John", "Paul", "George", "Ringo"]

georgeInBeatles : Elem "George" Beatles
georgeInBeatles = There (There Here)


text:
module Repmin

-- The repmin problem, based on http://www.springerlink.com/content/g74174vvl1861605/

map : (a -> b) -> Lazy a -> Lazy b
map f l = f l

fix : (Lazy a -> a) -> Lazy a
fix f = loop
  where
    loop : Lazy a
    loop = f loop

trace : (a -> Lazy b -> (c, b)) -> a -> c
trace f x = fst $ fix (\rec => f x (map snd rec))

data Tree a = Leaf a | Branch (Tree a) (Tree a)

copy : Tree Int -> Lazy Int -> (Tree (Lazy Int), Int)
copy (Leaf x) l = (Leaf l, x)
copy (Branch x y) l = let (tl, ml) = copy x l
                          (tr, mr) = copy y l in
                          (Branch tl tr, min ml mr)

repmin : Tree Int -> Tree (Lazy Int)
repmin t = trace copy t

print : Tree (Lazy Int) -> String
print (Leaf x) = "L " ++ (show x)
print (Branch x y) = "(B " ++ print x ++ " " ++ print y ++ ")"

test : String
test = print . repmin $ Branch (Branch (Leaf 0) (Leaf 2)) (Leaf 1)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
-- ---------------------------------------------------------------- [ Edda.idr ]
-- Module    : Edda.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.Pattern.Convert.String

import GRL.Lang.GLang

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern.API

-- -------------------------------------------------------------- [ Directives ]

%access private
%default partial

convertReq : REQUIREMENT impl d -> String
convertReq r = with SifExpr
    unwords [ "   "
             , show (getRTy r)
             , ":"
             , show (getTitle r)]

convertProblem : PROBLEM impl d -> String
convertProblem p = with SifExpr
    unwords [ "  problem:", show (getTitle p), "\n"
            , unlines $ map (convertReq) (getReqs p)
            , "\n"]

convertAffect : AFFECT impl d -> String
convertAffect a = with SifExpr
    unwords [ "       "
            , show (getCValue a), (getTitle $ getReq a), "\n"]

convertTrait : TRAIT impl d -> String
convertTrait t = with SifExpr
    unwords [
        "     "
        , show (getTTy t), ":"
        , show (getTitle t)
        , "is", show (getSValue t)
        , "\n"
      , concatMap (convertAffect) (getAffects t)
      , "\n"]

convertProperty : PROPERTY impl d -> String
convertProperty p = with SifExpr
    unwords [
        "     property: " , (getTitle p) , "\n"
     , concatMap (convertTrait) (getTraits p)
     , "\n"]

convertSolution : SOLUTION impl d -> String
convertSolution s = with SifExpr
    unwords [
         "  solution: " , (getTitle s) , "\n"
      , concatMap convertProperty (getProperties s)
      , "\n"]

convertContext : SifDomain -> String
convertContext (MkDomain t d) =
    unwords [ "  context:"
            , show t
            , "\n"]

convertPattern : PATTERN impl d -> String
convertPattern p =
    unwords [
         "Pattern:" , show (SifExpr.getTitle p) , "\n"
      , convertContext  $ SifExpr.getDomain p
      , convertProblem  $ SifExpr.getProblem p
      , convertSolution $ SifExpr.getSolution p]

namespace Sif
  export
  toString : PATTERN impl d -> String
  toString p = convertPattern p

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Main

import Libra.CLI

import Effects
-- Remember to import all the kinds of Effect's you're using:
import Effect.StdIO
import Effect.System
import Effect.File

main : IO ()
main = run cli

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module Uninh

data MyElem : a -> List a -> Type where
  MyHere : MyElem x (x :: xs)
  MyThere : (later : MyElem x xs) -> MyElem x (y :: xs)

noIndent : (MyElem a []) -> Void
noIndent c = ?noIndent_rhs

Uninhabited (MyElem a []) where
  uninhabited c = ?uninhabited_rhs


text:
module Data.Scientific
-- TODO: don't export everything publicly?

import Data.Fin
import Data.List

public export
data Coefficient : (b : Nat) -> Type where
  CoeffInt : Fin (S b) ->
             Coefficient (S (S b))
  CoeffFloat : Fin (S b) ->
               List (Fin (S (S b))) ->
               Fin (S b) ->
               Coefficient (S (S b))

public export
Eq (Coefficient b) where
  (CoeffInt x) == (CoeffInt y) = x == y
  (CoeffFloat x xs x') == (CoeffFloat y ys y') = x == y && xs == ys && x' == y'
  _ == _ = False

public export
Ord (Coefficient b) where
  compare (CoeffInt x) (CoeffInt y) = compare x y
  compare (CoeffInt x) (CoeffFloat y ys y') = case compare x y of
                                               EQ => LT
                                               comp => comp
  compare (CoeffFloat x xs x') (CoeffInt y) = case compare x y of
                                               EQ => GT
                                               comp => comp
  compare (CoeffFloat x xs x') (CoeffFloat y ys y') =
    compare (FS x :: xs `snoc` FS x') (FS y :: ys `snoc` FS y')

private
prettyShowDigit : Fin 10 -> Char
prettyShowDigit x =
  case x of
       0 => '0'
       1 => '1'
       2 => '2'
       3 => '3'
       4 => '4'
       5 => '5'
       6 => '6'
       7 => '7'
       8 => '8'
       9 => '9'

private
prettyShowCoefficient : Coefficient 10 -> String
prettyShowCoefficient (CoeffInt x) = pack [ prettyShowDigit (FS x) ]
prettyShowCoefficient (CoeffFloat x xs x') =
  pack $ [ prettyShowDigit (FS x), '.' ] ++ map prettyShowDigit xs ++ [ prettyShowDigit (FS x') ]

public export
data Sign = Positive
          | Negative

public export
Eq Sign where
  Positive == Positive = True
  Negative == Negative = True
  _ == _ = False

public export
Ord Sign where
  compare Positive Positive = EQ
  compare Positive Negative = GT
  compare Negative Positive = LT
  compare Negative Negative = EQ

private
prettyShowSign : Sign -> String
prettyShowSign s = case s of
                        Positive => ""
                        Negative => "-"

public export
data Scientific : (b : Nat) -> Type where
  SciZ : Scientific b
  Sci : Sign ->
        Coefficient b ->
        Integer ->
        Scientific b

public export
Eq (Scientific b) where
  SciZ == SciZ = True
  (Sci s c e) == (Sci s' c' e') = s == s' && c == c' && e == e'
  _ == _ = False

public export
Ord (Scientific b) where
  compare SciZ SciZ = EQ
  compare SciZ (Sci s _ _) = case s of
                                  Positive => LT
                                  Negative => GT
  compare (Sci s _ _) SciZ = case s of
                                  Positive => GT
                                  Negative => LT
  compare (Sci s c e) (Sci s' c' e') =
    case (s, s') of
         (Positive, Positive) => case compare e e' of
                                      EQ => compare c c'
                                      comp => comp
         (Positive, Negative) => GT
         (Negative, Positive) => LT
         (Negative, Negative) => case compare e' e of
                                      EQ => compare c' c
                                      comp => comp

export
negate : Scientific b -> Scientific b
negate SciZ = SciZ
negate (Sci s c e) = let s' = case s of
                                   Positive => Negative
                                   Negative => Positive
                     in Sci s' c e

export
abs : Scientific b -> Scientific b
abs SciZ = SciZ
abs (Sci _ c e) = Sci Positive c e

-- TODO: What happens, when Integer is negative? Low priority, since this is private.
private
||| The digits of an Integer, least significant first.
integerDigits : {b : _} -> Integer -> List (Fin (S (S b)))
integerDigits 0 = []
integerDigits x = d :: integerDigits r where
  d : Fin (S (S b))
  d = restrict (S b) x
  r : Integer
  r = x `div` natToInteger (S (S b))

private
removeLeadingZeros : List (Fin (S (S b))) -> Maybe (Fin (S b), List (Fin (S (S b))))
removeLeadingZeros [] = Nothing
removeLeadingZeros (FZ :: xs) = removeLeadingZeros xs
removeLeadingZeros (FS x :: xs) = Just (x, xs)

private
fromDigits : List (Fin (S (S b))) -> Scientific (S (S b))
fromDigits ys =
  case removeLeadingZeros $ reverse ys of
       Nothing => SciZ
       Just (x, ys') => case removeLeadingZeros $ reverse ys' of
                            Nothing => Sci Positive (CoeffInt x) (cast $ length ys')
                            Just (x', xs) => Sci Positive (CoeffFloat x (reverse xs) x') (cast $ length ys')

export
fromFin : Fin (S (S b)) -> Scientific (S (S b))
fromFin FZ = SciZ
fromFin (FS x) = Sci Positive (CoeffInt x) 0

export
fromInteger : {b : _} -> Integer -> Scientific (S (S b))
fromInteger x = if x < 0
                   then negate $ fromIntegerPositive x
                   else fromIntegerPositive x
where
  fromIntegerPositive : Integer -> Scientific (S (S b))
  fromIntegerPositive = fromDigits . integerDigits . abs

export
fromNat : {b : _} -> Nat -> Scientific (S (S b))
fromNat = fromInteger . natToInteger

||| All bits of a Coefficient, least significant first.
coefficientBits : Coefficient (S (S b)) -> List (Fin (S (S b)))
coefficientBits (CoeffInt x) = [FS x]
coefficientBits (CoeffFloat x xs x') = reverse $ FS x :: xs ++ [FS x']

-- TODO: currently add and subtract require equal lengths for the coefficients
-- adds 1 bit (might be zero)
addBits : {b : _} ->
          (carry : Bool) ->
          List (Fin (S (S b))) ->
          List (Fin (S (S b))) ->
          List (Fin (S (S b)))
addBits False [] [] = [FZ]
addBits True [] [] = [FS FZ]
addBits carry p@[] q@(y :: ys) = addBits carry q p -- TODO: case can be avoided when one is larger than the other
addBits False (x :: xs) [] = x :: addBits False xs []
addBits True (x :: xs) [] = case strengthen $ FS x of
                                 Left _ => FZ :: addBits True xs []
                                 Right x' => x' :: addBits False xs []
addBits carry (x :: xs) (y :: ys) =
  restrict (S b) addition :: addBits (addition >= natToInteger (S (S b))) xs ys where
    addition : Integer
    addition = if carry
                  then finToInteger x + finToInteger y + 1
                  else finToInteger x + finToInteger y

subtractBits : {b : _} ->
               (borrow : Bool) ->
               List (Fin (S (S b))) ->
               List (Fin (S (S b))) ->
               List (Fin (S (S b)))
subtractBits False [] [] = [FZ]
subtractBits True [] [] = ?thatShouldntHappen1
subtractBits borrow [] (x :: xs) = ?thatShouldntHappen2
subtractBits False (x :: xs) [] = x :: subtractBits False xs []
subtractBits True (FZ :: xs) [] = last :: subtractBits True xs []
subtractBits True ((FS x) :: xs) [] = weaken x :: subtractBits False xs []
subtractBits borrow (x :: xs) (y :: ys) = ?subtractBits_rhs_4

export
plus : {b : _} -> Scientific (S (S b)) -> Scientific (S (S b)) -> Scientific (S (S b))
plus SciZ y = y
plus x SciZ = x
-- TODO: finish plus
plus x@(Sci s c e) y@(Sci s' c' e') =
  case compare e e' of
       GT => plus y x
       _ => ?asdasd where
         exponentDifference : Nat
         exponentDifference = integerToNat $ e' - e
         bits : List (Fin (S (S b)))
         bits = addBits False (coefficientBits c ++ replicate exponentDifference FZ) (coefficientBits c')
         s'' : Sign
         c'' : Coefficient (S (S b))
         e'' : Integer
         e'' = e' + ?additionalExponent bits

||| Multiply two Coefficients and return True in the Bool, when the product is greater than the base.
multCoefficents : {b : _} -> Coefficient (S (S b)) -> Coefficient (S (S b)) -> (Coefficient (S (S b)), Bool)
multCoefficents (CoeffInt x) (CoeffInt y) =
  case integerToFin res (S b) of
       Nothing => (CoeffInt $ restrict b res, True)
       Just fin => (CoeffInt fin, False)
where
  res : Integer
  res = (finToInteger x + 1) * (finToInteger y + 1) - 1
multCoefficents a@(CoeffInt x) b@(CoeffFloat y ys y') = multCoefficents b a
-- TODO: finish multCoefficents
multCoefficents (CoeffFloat x xs x') (CoeffInt y) = ?multCoefficents_rhs_2
multCoefficents (CoeffFloat x xs x') (CoeffFloat y ys y') = ?multCoefficents_rhs_3

export
mult : {b : _} -> Scientific (S (S b)) -> Scientific (S (S b)) -> Scientific (S (S b))
mult SciZ y = SciZ
mult x SciZ = SciZ
mult (Sci s c e) (Sci s' c' e') = Sci s'' c'' e'' where
  coefficientPair : (Coefficient (S (S b)), Bool)
  coefficientPair = multCoefficents c c'
  s'' : Sign
  s'' = if s == s'
           then Positive
           else Negative
  c'' : Coefficient (S (S b))
  c'' = fst coefficientPair
  e'' : Integer
  e'' = if snd coefficientPair
           then e + e' + 1
           else e + e'

-- -- TODO: consider other implementations:
-- -- - Fractional might not terminate, because of infinite representation
-- -- - Integral doesn't sound like it would fit, but mod and div make still make sense
-- public export
-- Num (Scientific (S (S b))) where
--   -- (+) = plus
--   -- (*) = mult
--   -- fromInteger = fromInteger

--public export
--Neg (Scientific (S (S b))) where
--  -- negate = negate

--public export
--Abs (Scientific (S (S b))) where
--  -- abs = abs

export
prettyShowScientific : Scientific 10 -> String
prettyShowScientific SciZ = "0"
prettyShowScientific (Sci s c e) = prettyShowSign s ++ prettyShowCoefficient c ++ prettyExponent where
  prettyExponent : String
  prettyExponent = case e of
                        0 => ""
                        x => "e" ++ show x


text:
module TypeFuns

import Data.Strings

%default total

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Hello"
getStringOrInt True = 100

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False s = trim s
valToString True i = cast i

-- we can have practically any valid form in the type signature

valToStringCase : (isInt : Bool) -> (case isInt of False => String
                                                   True => Int) -> String
valToStringCase False s = trim s
valToStringCase True i = cast i

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Language.JSON.String.Parser

import Language.JSON.String.Tokens
import Text.Lexer
import Text.Parser

%default total

private
stringChar : Grammar state JSONStringToken True Char
stringChar = match JSTChar
         <|> match JSTSimpleEscape
         <|> match JSTUnicodeEscape

private
quotedString : Grammar state JSONStringToken True String
quotedString = let q = match JSTQuote in
                   do chars <- between q q (many stringChar)
                      eof
                      pure $ pack chars

export
parseString : List (WithBounds JSONStringToken) -> Maybe String
parseString toks = case parse quotedString toks of
                        Right (str, []) => Just str
                        _ => Nothing


text:
%language UniquenessTypes

data UList : Type -> UniqueType where
    Nil : UList a
    (::) : a -> UList a -> UList a

umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs

dupList : UList a -> UList a
dupList [] = []
dupList (x :: xs) = x :: x :: dupList xs

-- data BadList : UniqueType -> Type where
--     Nil : {a : UniqueType} -> BadList a
--     (::) : {a : UniqueType} -> a -> BadList a -> BadList a

showU : Show a => Borrowed $ UList a -> String
showU xs = "[" ++ showU' xs ++ "]" where
    showU' : Borrowed $ UList a -> String
    showU' [] = ""
    showU' [x] = show x
    showU' (x :: xs) = show x ++ ", " ++ showU' xs

printAndUpdate : UList Int -> IO ()
printAndUpdate xs =
    do
        putStrLn $ showU xs
        let xs' = umap (* 2) xs
        putStrLn (showU xs')


text:
module Data.Fin

import Data.List1
import public Data.Maybe
import Data.Nat
import Decidable.Equality.Core

%default total

||| Numbers strictly less than some bound.  The name comes from "finite sets".
|||
||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
||| exceedingly inefficient at run time.
||| @ n the upper bound
public export
data Fin : (n : Nat) -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

||| Coerce between Fins with equal indices
public export
coerce : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n
coerce {n = S _} eq FZ = FZ
coerce {n = Z} eq FZ impossible
coerce {n = S _} eq (FS k) = FS (coerce (succInjective _ _ eq) k)
coerce {n = Z} eq (FS k) impossible

%transform "coerce-identity" coerce = replace {p = Fin}

export
Uninhabited (Fin Z) where
  uninhabited FZ impossible
  uninhabited (FS f) impossible

export
Uninhabited (FZ = FS k) where
  uninhabited Refl impossible

export
Uninhabited (FS k = FZ) where
  uninhabited Refl impossible

export
Uninhabited (n = m) => Uninhabited (FS n = FS m) where
  uninhabited Refl @{nm} = uninhabited Refl @{nm}

export
fsInjective : FS m = FS n -> m = n
fsInjective Refl = Refl

export
Eq (Fin n) where
    (==) FZ FZ = True
    (==) (FS k) (FS k') = k == k'
    (==) _ _ = False

||| Convert a Fin to a Nat
public export
finToNat : Fin n -> Nat
finToNat FZ = Z
finToNat (FS k) = S $ finToNat k

||| `finToNat` is injective
export
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
finToNatInjective FZ     FZ     _    = Refl
finToNatInjective (FS _) FZ     Refl impossible
finToNatInjective FZ     (FS _) Refl impossible
finToNatInjective (FS m) (FS n) prf  =
  cong FS $ finToNatInjective m n $ succInjective (finToNat m) (finToNat n) prf

export
Cast (Fin n) Nat where
    cast = finToNat

||| Convert a Fin to an Integer
public export
finToInteger : Fin n -> Integer
finToInteger FZ     = 0
finToInteger (FS k) = 1 + finToInteger k

-- %builtin NaturalToInteger Data.Fin.finToInteger

export
Show (Fin n) where
  show = show . finToInteger

export
Cast (Fin n) Integer where
    cast = finToInteger

||| Weaken the bound on a Fin by 1
public export
weaken : Fin n -> Fin (S n)
weaken FZ     = FZ
weaken (FS k) = FS $ weaken k

||| Weaken the bound on a Fin by some amount
public export
weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)
weakenN n FZ = FZ
weakenN n (FS f) = FS $ weakenN n f

||| Weaken the bound on a Fin using a constructive comparison
public export
weakenLTE : Fin n -> LTE n m -> Fin m
weakenLTE  FZ     LTEZero impossible
weakenLTE (FS _)  LTEZero impossible
weakenLTE  FZ    (LTESucc _) = FZ
weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y

||| Attempt to tighten the bound on a Fin.
||| Return the tightened bound if there is one, else nothing.
export
strengthen : {n : _} -> Fin (S n) -> Maybe (Fin n)
strengthen {n = S _} FZ = Just FZ
strengthen {n = S _} (FS p) with (strengthen p)
  strengthen (FS _) | Nothing = Nothing
  strengthen (FS _) | Just q  = Just $ FS q
strengthen _ = Nothing

||| Add some natural number to a Fin, extending the bound accordingly
||| @ n the previous bound
||| @ m the number to increase the Fin by
public export
shift : (m : Nat) -> Fin n -> Fin (m + n)
shift Z f = f
shift (S m) f = FS $ shift m f

||| The largest element of some Fin type
public export
last : {n : _} -> Fin (S n)
last {n=Z} = FZ
last {n=S _} = FS last

||| All of the Fin elements
public export
allFins : (n : Nat) -> List1 (Fin (S n))
allFins Z = FZ ::: []
allFins (S n) = FZ ::: map FS (forget (allFins n))

export
Ord (Fin n) where
  compare  FZ     FZ    = EQ
  compare  FZ    (FS _) = LT
  compare (FS _)  FZ    = GT
  compare (FS x) (FS y) = compare x y

public export
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin Z     (S _) = Just FZ
natToFin (S k) (S j) = FS <$> natToFin k j
natToFin _ _ = Nothing

||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
||| @n The upper bound of the Fin
public export
integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
integerToFin x n = if x >= 0 then natToFin (fromInteger x) n else Nothing

||| Allow overloading of Integer literals for Fin.
||| @ x the Integer that the user typed
||| @ prf an automatically-constructed proof that `x` is in bounds
public export
fromInteger : (x : Integer) -> {n : Nat} ->
              {auto 0 prf : (IsJust (integerToFin x n))} ->
              Fin n
fromInteger {n} x {prf} with (integerToFin x n)
  fromInteger {n} x {prf = ItIsJust} | Just y = y

-- %builtin IntegerToNatural Data.Fin.fromInteger

||| Convert an Integer to a Fin in the required bounds/
||| This is essentially a composition of `mod` and `fromInteger`
public export
restrict : (n : Nat) -> Integer -> Fin (S n)
restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
                     -- reasoning about primitives, so we need the
                     -- 'believe_me'. It's fine because val' must be
                     -- in the right range
                     fromInteger {n = S n} val'
                         {prf = believe_me {a=IsJust (Just val')} ItIsJust}

--------------------------------------------------------------------------------
-- DecEq
--------------------------------------------------------------------------------

public export
DecEq (Fin n) where
  decEq FZ FZ = Yes Refl
  decEq FZ (FS f) = No absurd
  decEq (FS f) FZ = No absurd
  decEq (FS f) (FS f')
      = case decEq f f' of
             Yes p => Yes $ cong FS p
             No p => No $ p . fsInjective

namespace Equality

  ||| Pointwise equality of Fins
  ||| It is sometimes complicated to prove equalities on type-changing
  ||| operations on Fins.
  ||| This inductive definition can be used to simplify proof. We can
  ||| recover proofs of equalities by using `homoPointwiseIsEqual`.
  public export
  data Pointwise : Fin m -> Fin n -> Type where
    FZ : Pointwise FZ FZ
    FS : Pointwise k l -> Pointwise (FS k) (FS l)

  infix 6 ~~~
  ||| Convenient infix notation for the notion of pointwise equality of Fins
  public export
  (~~~) : Fin m -> Fin n -> Type
  (~~~) = Pointwise

  ||| Pointwise equality is reflexive
  export
  reflexive : {k : Fin m} -> k ~~~ k
  reflexive {k = FZ} = FZ
  reflexive {k = FS k} = FS reflexive

  ||| Pointwise equality is symmetric
  export
  symmetric : k ~~~ l -> l ~~~ k
  symmetric FZ = FZ
  symmetric (FS prf) = FS (symmetric prf)

  ||| Pointwise equality is transitive
  export
  transitive : j ~~~ k -> k ~~~ l -> j ~~~ l
  transitive FZ FZ = FZ
  transitive (FS prf) (FS prg) = FS (transitive prf prg)

  ||| Pointwise equality is compatible with coerce
  export
  coerceEq : {k : Fin m} -> (0 eq : m = n) -> coerce eq k ~~~ k
  coerceEq {k = FZ} Refl = FZ
  coerceEq {k = FS k} Refl = FS (coerceEq _)

  ||| The actual proof used by coerce is irrelevant
  export
  congCoerce : {0 n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
               {0 eq1 : m = n} -> {0 eq2 : p = q} ->
               k ~~~ l ->
               coerce eq1 k ~~~ coerce eq2 l
  congCoerce eq
    = transitive (coerceEq _)
    $ transitive eq $ symmetric $ coerceEq _

  ||| Last is congruent wrt index equality
  export
  congLast : {m : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
  congLast Refl = reflexive

  export
  congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l
  congShift Z prf = prf
  congShift (S m) prf = FS (congShift m prf)

  ||| WeakenN is congruent wrt pointwise equality
  export
  congWeakenN : k ~~~ l -> weakenN n k ~~~ weakenN n l
  congWeakenN FZ = FZ
  congWeakenN (FS prf) = FS (congWeakenN prf)

  ||| Pointwise equality is propositional equality on Fins that have the same type
  export
  homoPointwiseIsEqual : {0 k, l : Fin m} -> k ~~~ l -> k === l
  homoPointwiseIsEqual FZ = Refl
  homoPointwiseIsEqual (FS prf) = cong FS (homoPointwiseIsEqual prf)

  ||| Pointwise equality is propositional equality modulo transport on Fins that
  ||| have provably equal types
  export
  hetPointwiseIsTransport :
     {0 k : Fin m} -> {0 l : Fin n} ->
     (0 eq : m === n) -> k ~~~ l -> k === rewrite eq in l
  hetPointwiseIsTransport Refl = homoPointwiseIsEqual

  export
  finToNatQuotient : k ~~~ l -> finToNat k === finToNat l
  finToNatQuotient FZ = Refl
  finToNatQuotient (FS prf) = cong S (finToNatQuotient prf)

  export
  weakenNeutral : (k : Fin n) -> weaken k ~~~ k
  weakenNeutral FZ = FZ
  weakenNeutral (FS k) = FS (weakenNeutral k)

  export
  weakenNNeutral : (0 m : Nat) -> (k : Fin n) -> weakenN m k ~~~ k
  weakenNNeutral m FZ = FZ
  weakenNNeutral m (FS k) = FS (weakenNNeutral m k)


text:
import AutoHotkey.Builtins
import AutoHotkey.FFI

foo : String
foo =
  let x = \y => y ++ "from Idris!"
  in x "Hello AutoHotkey, "

main : AHK_IO ()
main = msgBox foo

max_stars_repo_name: joedf/idris-autohotkey

max_issues_repo_name: joedf/idris-autohotkey

max_forks_repo_name: joedf/idris-autohotkey


text:
import Data.List

data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

wrong : String
wrong = show (the (Vect _ _) [1,2,3,4])


text:
-- Copyright (c) 2013 Radek Micek

module TestSolver

import Common
import Solver

instance (Eq a, Eq b) => Eq (Either a b) where
  (Left x) == (Left y) = x == y
  (Right x) == (Right y) = x == y
  _ == _ = False

-- ---------------------------------------------------------------------------
-- Parser

test_parseLit_pos : so $ parseLit "c" == Right (MkLit Pos "c")
test_parseLit_pos = oh

test_parseLit_pos2 : so $ parseLit "Long_name" == Right (MkLit Pos "Long_name")
test_parseLit_pos2 = oh

test_parseLit_neg : so $ parseLit "!b" == Right (MkLit Neg "b")
test_parseLit_neg = oh

test_parseLit_neg2 : so $ parseLit "~X" == Right (MkLit Neg "X")
test_parseLit_neg2 = oh

test_parseLit_neg3 : so $ parseLit "~_" == Right (MkLit Neg "_")
test_parseLit_neg3 = oh

test_parseLit_empty : so $ isLeft $ parseLit ""
test_parseLit_empty = oh

test_parseLit_bad : so $ isLeft $ parseLit "~~a"
test_parseLit_bad = oh

test_parseLit_bad2 : so $ isLeft $ parseLit "1a"
test_parseLit_bad2 = oh

test_parseLits : so $ parseLits "a, ~a" == Right [MkLit Pos "a", MkLit Neg "a"]
test_parseLits = oh

test_parseLits2 : so $ parseLits "~lit | " == Right [MkLit Neg "lit"]
test_parseLits2 = oh

test_parseLits3 : so $ parseLits "a , ~b | c"
                         == Right [MkLit Pos "a", MkLit Neg "b", MkLit Pos "c"]
test_parseLits3 = oh

test_parseLits_bad : so $ isLeft $ parseLits "a | ~b | | ~c"
test_parseLits_bad = oh

-- ---------------------------------------------------------------------------
-- Minimization

minim_clauses : List Clause
minim_clauses =
  [ MkClause (MkCId 1) [MkLit Pos "a"]
  , MkClause (MkCId 2) [MkLit Pos "b"]
  , MkClause (MkCId 3) [MkLit Neg "a", MkLit Neg "c", MkLit Pos "d"]
  , MkClause (MkCId 4) [MkLit Neg "b", MkLit Neg "d", MkLit Pos "e"]
  , MkClause (MkCId 5) [MkLit Neg "d", MkLit Neg "f", MkLit Pos "g"]
  , MkClause (MkCId 6) [MkLit Neg "e", MkLit Neg "g", MkLit Pos "h"]
  , MkClause (MkCId 7) [MkLit Neg "h", MkLit Pos "i"]
  , MkClause (MkCId 8) [MkLit Neg "k", MkLit Pos "l"]
  , MkClause (MkCId 9) [MkLit Neg "l", MkLit Neg "r", MkLit Pos "s"]
  , MkClause (MkCId 10) [ MkLit Neg "d", MkLit Neg "g"
                        , MkLit Neg "s", MkLit Pos "t" ]
  , MkClause (MkCId 11) [MkLit Neg "s", MkLit Pos "x"]
  , MkClause (MkCId 12) [ MkLit Neg "h", MkLit Neg "i"
                        , MkLit Neg "t", MkLit Pos "y" ]
  , MkClause (MkCId 13) [MkLit Neg "x", MkLit Pos "z"]
  , MkClause (MkCId 14) [MkLit Neg "z", MkLit Neg "y"]
  ]

minim_trail : Trail
minim_trail =
  [ (MkLit Pos "z", Just $ MkCId 13, 4)
  , (MkLit Pos "y", Just $ MkCId 12, 4)
  , (MkLit Pos "x", Just $ MkCId 11, 4)
  , (MkLit Pos "t", Just $ MkCId 10, 4)
  , (MkLit Pos "s", Just $ MkCId 9, 4)
  , (MkLit Pos "r", Nothing, 4)
  , (MkLit Pos "l", Just $ MkCId 8, 3)
  , (MkLit Pos "k", Nothing, 3)
  , (MkLit Pos "i", Just $ MkCId 7, 2)
  , (MkLit Pos "h", Just $ MkCId 6, 2)
  , (MkLit Pos "g", Just $ MkCId 5, 2)
  , (MkLit Pos "f", Nothing, 2)
  , (MkLit Pos "e", Just $ MkCId 4, 1)
  , (MkLit Pos "d", Just $ MkCId 3, 1)
  , (MkLit Pos "c", Nothing, 1)
  , (MkLit Pos "b", Just $ MkCId 2, 0)
  , (MkLit Pos "a", Just $ MkCId 1, 0)
  ]

minim_sol : Sol
minim_sol = record
              { sClauses = minim_clauses
              , sLevel = 4
              , sTrail = minim_trail }
            emptySol

runMinim : Sol -> List Lit -> (List Lit, List Event)
runMinim s assertingCl = run' [] $ run s $ minimize assertingCl
  where
    run' : List i -> AlgoResult Sol i r -> (r, List i)
    run' is (Interrupt s i k) = run' (i :: is) $ resume s k
    run' is (Finish _ r) = (r, is)

minim_assertingCl : List Lit
minim_assertingCl =
  [ MkLit Neg "d"
  , MkLit Neg "g"
  , MkLit Neg "h"
  , MkLit Neg "i"
  , MkLit Neg "s"
  ]

minim_minimizedAssertingCl : List Lit
minim_minimizedAssertingCl =
  [ MkLit Neg "d"
  , MkLit Neg "g"
  , MkLit Neg "s"
  ]

test_minim : so $ fst (runMinim minim_sol minim_assertingCl)
                    == minim_minimizedAssertingCl
test_minim = oh

-- ---------------------------------------------------------------------------
-- Solver

solveProb : Sol -> SatAlgo Result () -> (Result, Assignment, List Event)
solveProb sol prob = solve' [] $ run sol (prob $> solve)
  where
    solve' :
      List Event ->
      AlgoResult Sol Event r ->
      (r, Assignment, List Event)
    solve' is (Interrupt s (EChoose (v :: vs)) k) =
      solve'
        (EChoose (v :: vs) :: is)
        (resume (record { sChosen = Just $ MkLit Pos v } s) k)
    solve' is (Interrupt s i k) = solve' (i :: is) $ resume s k
    solve' is (Finish s r) = (r, trailToAssig $ sTrail s, is)

isSat' : SatAlgo Result () -> List (List Lit) -> Sol -> Bool
isSat' prob lits sol = case solveProb sol prob of
  (Sat, assig, _) =>
    -- Some list of literals in lits is satisfied by assig.
    any (List.all $ \l => assig l == LTrue) lits
  _ => False

isUnsat' : SatAlgo Result () -> Sol -> Bool
isUnsat' prob sol = case solveProb sol prob of
  (Unsat, _, _) => True
  _ => False

configs : List Sol
configs = [ record { sEnableMinimization = False
                   , sEnableWatchedLits = False } emptySol
          , record { sEnableMinimization = True
                   , sEnableWatchedLits = False } emptySol
-- Needs a lot of memory.
--          , record { sEnableMinimization = False
--                   , sEnableWatchedLits = True } emptySol
          , record { sEnableMinimization = True
                   , sEnableWatchedLits = True } emptySol
          ]

isSat : SatAlgo Result () -> List (List Lit) -> Bool
isSat prob lits = all (isSat' prob lits) configs

isUnsat : SatAlgo Result () -> Bool
isUnsat prob = all (isUnsat' prob) configs

-- Satisfiable only by: a = 0, b = 0
--                      a = 0, b = 1
prob_sat : SatAlgo r ()
prob_sat = do
  addClause [MkLit Neg "a", MkLit Neg "b"]
  addClause [MkLit Neg "a", MkLit Pos "b"]
  return ()

test_solve_sat : so $ isSat prob_sat [ [MkLit Neg "a", MkLit Neg "b"]
                                     , [MkLit Neg "a", MkLit Pos "b"]
                                     ]
test_solve_sat = oh

-- Satisfiable only by: a = 0, b = 0
prob_sat2 : SatAlgo r ()
prob_sat2 = do
  addClause [MkLit Pos "a", MkLit Neg "b"]
  addClause [MkLit Neg "a", MkLit Neg "b"]
  addClause [MkLit Neg "a", MkLit Pos "b"]
  return ()

test_solve_sat2 : so $ isSat prob_sat2 [[MkLit Neg "a", MkLit Neg "b"]]
test_solve_sat2 = oh

prob_sat3 : SatAlgo r ()
prob_sat3 = return ()

test_solve_sat3 : so $ isSat prob_sat3 [[]]
test_solve_sat3 = oh

prob_unsat : SatAlgo r ()
prob_unsat = do
  addClause [MkLit Pos "a", MkLit Neg "b"]
  addClause [MkLit Neg "a", MkLit Neg "b"]
  addClause [MkLit Neg "a", MkLit Pos "b"]
  addClause [MkLit Pos "a", MkLit Pos "b"]
  return ()

test_solve_unsat : so $ isUnsat prob_unsat
test_solve_unsat = oh

prob_unsat2 : SatAlgo r ()
prob_unsat2 = do
  addClause []
  return ()

test_solve_unsat2 : so $ isUnsat prob_unsat2
test_solve_unsat2 = oh

php : Nat -> Nat -> SatAlgo r ()
php np nh = do
    -- Each pigeon is at least in one hole.
    mapM_ (\p => addClause $ map (ph Pos p) [1..nh]) [1..np]
    -- No hole contains two pigeons.
    let pigeonPairs = [(p, p2) | p <- [1..np], p2 <- [(p+1)..np]]
    mapM_
      (\h => mapM_ addClause
               $ map (\(p, p2) => [ph Neg p h, ph Neg p2 h]) pigeonPairs)
      [1..nh]
    -- No pigeon is in two holes.
    let holePairs = [(h, h2) | h <- [1..nh], h2 <- [(h+1)..nh]]
    mapM_
      (\p => mapM_ addClause
               $ map (\(h, h2) => [ph Neg p h, ph Neg p h2]) holePairs)
      [1..np]
  where
    ph : Sign -> Nat -> Nat -> Lit
    ph sign p h = MkLit sign $ "p" ++ show p ++ "h" ++ show h

test_solve_php32 : so $ isUnsat $ php 3 2
test_solve_php32 = oh

-- Needs massive amount of memory.
--test_solve_php43 : so $ isUnsat $ php 4 3
--test_solve_php43 = oh

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Typing

-- Typing judgement for the simply-typed lambda
-- calculus with
--   (1) natural numbers as the only base type, and
--   (2) general recursion.

import Term

%default total
%access public export

---------------------------------------------------
-- Begin: TYPES IN THE SIMPLY-TYPED LAMBDA CALCULUS

-- Data type 'Ty' represents the types in the
-- simply-typed lambda calculus:
--   (1) Base type 'TyNat' of natural numbers.
--   (2) Type constructor 'TyFun' for forming
--       function types.
data Ty = TyNat | TyFun Ty Ty

-- Simplified syntax for function types:
infixr 10 :->:
(:->:) : Ty -> Ty -> Ty
(:->:) t1 t2 = TyFun t1 t2

-- End: TYPES IN THE SIMPLY-TYPED LAMBDA CALCULUS
-------------------------------------------------

---------------------------------------------------------
-- Begin: CONTEXT FOR TYPING TERMS IN THE LAMBDA CALCULUS

Context : Type
Context = List Ty

-- End: CONTEXT FOR TYPING TERMS IN THE LAMBDA CALCULUS
-------------------------------------------------------

--------------------------
-- Begin: TYPING JUDGEMENT

data Typing : Context -> Term -> Ty -> Type where
  TyVar  : (prf : index' i ctx = Just t) ->
           Typing ctx (TVar i) t
  --
  TyAbs  : (s : Ty) ->
           Typing (s::ctx) e t ->
           Typing ctx (TAbs e) (s :->: t)
  --
  TyApp  : Typing ctx e1 (s :->: t) -> Typing ctx e2 s ->
           Typing ctx (TApp e1 e2) t
  --
  TyRec  : Typing ctx e1 TyNat -> Typing ctx e2 t ->
           Typing ctx e3 (TyNat :->: t :->: t) ->
           Typing ctx (TRec e1 e2 e3) t
  --
  TyZero : Typing ctx TZero TyNat
  --
  TySucc : Typing ctx e TyNat ->
           Typing ctx (TSucc e) TyNat
  --
  TyPred : Typing ctx e TyNat ->
           Typing ctx (TPred e) TyNat
  --
  TyIfz  : Typing ctx e1 TyNat -> Typing ctx e2 t -> Typing ctx e3 t ->
           Typing ctx (TIfz e1 e2 e3) t

type : Typing ctx e t -> Ty
type {t} _ = t

-- End: TYPING JUDGEMENT
------------------------

-------------------------
-- Begin: CANONICAL FORMS

canonicalNat : (e : Term) ->
               Typing ctx e TyNat ->
               Value e ->
               Either (e = TZero) (e' : Term ** (Value e', e = TSucc e'))
canonicalNat (TVar i) (TyVar prf) v impossible
canonicalNat (TApp e1 e2) (TyApp ty1 ty2) v impossible
canonicalNat (TRec e1 e2 e3) (TyRec ty1 ty2 ty3) v impossible
canonicalNat TZero TyZero v = Left Refl
canonicalNat (TSucc e) (TySucc ty) (VSucc v) =
  let ih = canonicalNat e ty v
  in case ih of
    (Left eq) => let eq' = cong {f = TSucc} eq
                 in Right (TZero ** (VZero, eq'))
    (Right (e1 ** (v1, eq))) => let e'  = TSucc e1
                                    v'  = VSucc v1
                                    eq' = cong {f = TSucc} eq
                                in Right (e' ** (v', eq'))
canonicalNat (TPred e) (TyPred ty) v impossible
canonicalNat (TIfz e1 e2 e3) (TyIfz ty1 ty2 ty3) v impossible

canonicalFun : (e : Term) ->
               Typing ctx e (s :->: t) ->
               Value e ->
               (e' : Term ** (e = TAbs e'))
canonicalFun (TVar i) (TyVar prf) v impossible
canonicalFun (TAbs e) (TyAbs s ty) v = (e ** Refl)
canonicalFun (TApp e1 e2) (TyApp ty1 ty2) v impossible
canonicalFun (TRec e1 e2 e3) (TyRec ty1 ty2 ty3) v impossible
canonicalFun (TIfz e1 e2 e3) (TyIfz ty1 ty2 ty3) v impossible

-- End: CANONICAL FORMS
-----------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module IdrTest.Test

import Data.List
import Data.Maybe
import Data.SortedSet as Set
import Extra.String
import IdrTest.Expectation
import System

data Flag : Type where
  Only : Flag
  Skip : Flag

Eq Flag where
  Only == Only = True
  Skip == Skip = True
  _ == _ = False

Ord Flag where
  compare Only Skip = GT
  compare Skip Only = LT
  compare _ _ = EQ

TestCase : Type
TestCase = (String, () -> Expectation, SortedSet Flag)

export
Test : Type
Test = List TestCase

toTestList : Test -> List TestCase
toTestList = id

runTest : (Nat, List String) -> TestCase -> (Nat, List String)
runTest (succ, failures) (name, expectation, _) =
  case expectation () of
    Nothing =>
      (succ + 1, failures)
    Just err =>
      (succ, (name ++ ": " ++ err) :: failures)

enumerate : Nat -> String -> String -> String
enumerate n single multiple =
  (show n) ++ " " ++ case n of
    1 =>
      single
    _ =>
      multiple

showResults : (Nat, List String) -> Nat -> IO ()
showResults (succ, failures) skips =
  let
    count = succ + List.length failures + skips
    countStr = enumerate count "test" "tests"
    successStr = enumerate succ "success" "successes"
    failureStr = enumerate (List.length failures) "failure" "failures"
    skipStr = enumerate skips "test skipped" "tests skipped"
    allFailuresStr = join "\n\n" $ map (\f => "❌ Failed: " ++ f) failures
  in
    do putStrLn allFailuresStr
       putStrLn (join ", " [countStr, successStr, failureStr, skipStr])

export
describe : String -> (List Test) -> Test
describe desc =
  map (\(name, expectation) => (desc ++ ": " ++ name, expectation)) . concat

export
only : Test -> Test
only =
  map (\(name, expectation, flags) => (name, expectation, insert Only flags))

export
skip : Test -> Test
skip =
  map (\(name, expectation, flags) => (name, expectation, insert Skip flags))

export
test : String -> (() -> Expectation) -> Test
test name expectation =
  [
    (name, expectation, Set.empty)
  ]

filterTests : List TestCase -> (List TestCase, List TestCase)
filterTests tests =
  let
    cond = if hasOnly tests
      then filterForOnly
      else filterSkips
  in
    partition cond tests
  where
    hasOnly : List TestCase -> Bool
    hasOnly =
      any (\(_, _, f) => Set.contains Only f)

    filterSkips : TestCase -> Bool
    filterSkips (_, _, flags) =
      not $ Set.contains Skip flags

    filterForOnly : TestCase -> Bool
    filterForOnly (_, _, flags) =
      Set.contains Only flags && (not $ Set.contains Skip flags)

export
runSuite : Test -> IO Bool
runSuite suite =
  let
    (tests, skips) = filterTests (toTestList suite)
    results = foldl runTest (0, []) tests
  in
    do
      showResults results (List.length skips)
      pure $ ((length . snd) results > 0) -- has failures

export
runSuites : List Test -> IO ()
runSuites tests =
  do
    hasFailures <- (runSuite . concat) tests
    if hasFailures
      then exitFailure
      else exitSuccess

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- dequeue should get the same thing back

import System.Concurrency.Queue

main : IO ()
main = do q <- makeQueue {a=Nat}
          let val = 3
          enqueue q val
          (Just n) <- dequeue q
            | Nothing => putStrLn "ERROR: Value disappeared from queue."
          if n == val
             then putStrLn "Success!"
             else putStrLn "ERROR: Value changed between en- and de-queue."


text:
module IntShow

-- This file to be deleted once these interfaces are added to prelude

firstCharIs : (Char -> Bool) -> String -> Bool
firstCharIs p "" = False
firstCharIs p str = p (assert_total (prim__strHead str))

primNumShow : (a -> String) -> Prec -> a -> String
primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str

export
Show Int8 where
  showPrec = primNumShow prim__cast_Int8String

export
Show Int16 where
  showPrec = primNumShow prim__cast_Int16String

export
Show Int32 where
  showPrec = primNumShow prim__cast_Int32String

export
Show Int64 where
  showPrec = primNumShow prim__cast_Int64String

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
mid : {A:Type} -> A -> A
mid = \ x => x

CPair : Type -> Type -> Type
CPair = \ a, b => (p : Type) -> (a -> b -> p) -> p

cdup : {A:Type} -> A -> CPair A A
cdup = \ a, x, p => p a a

CNat : Type
CNat = (n : Type) -> (n -> n) -> n -> n

czero : CNat
czero = \ n, s, z => z

csuc : CNat -> CNat
csuc = \ a, n, s, z => s (a n s z)

CVec : Type -> CNat -> Type
CVec = \ a, n => (V : CNat -> Type) -> ({n : CNat} -> a -> V n -> V (csuc n)) -> V czero -> V n

cnil : {A:Type} -> CVec A Main.czero
cnil = \ v, c, n => n

ccons : {A:Type}->{n:CNat} -> A -> CVec A n -> CVec A (csuc n)
ccons = \ a, as, v, c, n => c a (as v c n)

--------------------------------------------------------------------------------

-- fails
-- idTest : {A:Type} -> A -> A
-- idTest =
--     mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid
--     mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid mid

-- fails
-- pairTest =
--   let x0  = cdup Type
--       x1  = cdup x0
--       x2  = cdup x1
--       x3  = cdup x2
--       x4  = cdup x3
--       x5  = cdup x4
--       x6  = cdup x5
--       x7  = cdup x6
--       x8  = cdup x7
--       x9  = cdup x8
--       x10 = cdup x9
--       x11 = cdup x10
--       x12 = cdup x11
--       x13 = cdup x12
--       x14 = cdup x13
--       x15 = cdup x14
--       x16 = cdup x15
--       x17 = cdup x16
--       x18 = cdup x17
--       x19 = cdup x18
--       x20 = cdup x19
--       x21 = cdup x20
--       x22 = cdup x21
--       x23 = cdup x22
--       x24 = cdup x23
--       x25 = cdup x24
--       x26 = cdup x25
--       x27 = cdup x26
--       x28 = cdup x27
--       x29 = cdup x28
--       x30 = cdup x29
--   in x30

vecTest : Type
vecTest =
  let foo =
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type
       (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type (ccons Type

       cnil

       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))

  in Type

max_stars_repo_name: Kha/smalltt

max_issues_repo_name: Kha/smalltt

max_forks_repo_name: Kha/smalltt


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 9

-- check that all functions are total
  %default total

--
-- section 9.1
--

data Elem' : a -> List a -> Type where
  Here : Elem' x (x :: xs)
  There : Elem' x xs -> Elem' x (y :: xs)

-- > the (Elem' 2 [1, 2, 4]) (There Here)
-- There Here : Elem' 2 [1, 2, 4]
-- > the (Elem' 7 [1, 2, 4]) (There Here)
-- (input):1:26-35:When checking an application of constructor Main.There:
--         Type mismatch between
--                 Elem' 2 [2, 4] (Type of Here)
--         and
--                 Elem' 7 [2, 4] (Expected type)
--
--         Specifically:
--                 Type mismatch between
--                         2
--                 and
--                         7

data Last : List a -> a -> Type where
  LastOne : Last [value] value
  LastCons : (prf : Last xs value) -> Last (x :: xs) value

-- > the (Last [1,2,3] 3) $ LastCons (LastCons LastOne)
-- LastCons (LastCons LastOne) : Last [1, 2, 3] 3

noLastInEmpty : Last [] value -> Void
noLastInEmpty LastOne impossible
noLastInEmpty (LastCons _) impossible

noLastInLast : (contra : (x = value) -> Void) -> Last [x] value -> Void
noLastInLast contra LastOne = contra Refl
noLastInLast _ (LastCons LastOne) impossible
noLastInLast _ (LastCons (LastCons _)) impossible

noLastRec : (contra : Last (x :: xs) value -> Void) ->
            Last (y :: (x :: xs)) value -> Void
noLastRec contra (LastCons prf) = contra prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No noLastInEmpty
isLast [x] value = case decEq x value of
                              (Yes Refl) => Yes LastOne
                              (No contra) => No (noLastInLast contra)
isLast (y :: x :: xs) value = case isLast (x :: xs) value of
                              (Yes prf) => Yes (LastCons prf)
                              (No contra) => No (noLastRec contra)

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
data EitherOrBoth a b = Left a | Rigth b | Both a b

foo : EitherOrBoth a b -> ()