text:
module TTImp.Interactive.GenerateDef

-- Attempt to generate a complete definition from a type

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

import Parser.Lexer.Source

import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Interactive.CaseSplit
import TTImp.Interactive.ExprSearch
import TTImp.ProcessDecls
import TTImp.ProcessDef
import TTImp.TTImp
import TTImp.Unelab
import TTImp.Utils

import Data.List

%default covering

fnName : Bool -> Name -> String
fnName lhs (UN (Basic n))
    = if isIdentNormal n then n
      else if lhs then "(" ++ n ++ ")"
      else "op"
fnName lhs (NS _ n) = fnName lhs n
fnName lhs (DN s _) = s
fnName lhs n = nameRoot n

-- Make the hole on the RHS have a unique name
uniqueRHS : {auto c : Ref Ctxt Defs} ->
            ImpClause -> Core ImpClause
uniqueRHS (PatClause fc lhs rhs)
    = pure $ PatClause fc lhs !(mkUniqueName rhs)
  where
    mkUniqueName : RawImp -> Core RawImp
    mkUniqueName (IHole fc' rhsn)
        = do defs <- get Ctxt
             rhsn' <- uniqueName defs [] rhsn
             pure (IHole fc' rhsn')
    mkUniqueName tm = pure tm -- it'll be a hole, but this is needed for covering
uniqueRHS c = pure c

expandClause : {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               FC -> SearchOpts -> Int -> ImpClause ->
               Core (Search (List ImpClause))
expandClause loc opts n c
    = do c <- uniqueRHS c
         Right clause <- checkClause linear Private PartialOK False n [] (MkNested []) [] c
            | Left err => noResult -- TODO: impossible clause, do something
                                   -- appropriate

         let MkClause {vars} env lhs rhs = clause
         let Meta _ i fn _ = getFn rhs
            | _ => throw (GenericMsg loc "No searchable hole on RHS")
         defs <- get Ctxt
         Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs)
            | _ => throw (GenericMsg loc "No searchable hole on RHS")
         log "interaction.generate" 10 $ "Expression search for " ++ show (i, fn)
         rhs' <- exprSearchOpts opts loc (Resolved fn) []
         traverse (\rhs' =>
            do let rhsraw = dropLams locs rhs'
               logTermNF "interaction.generate" 5 "Got clause" env lhs
               log "interaction.generate" 5 $ "        = " ++ show rhsraw
               pure [updateRHS c rhsraw]) rhs'
  where
    updateRHS : ImpClause -> RawImp -> ImpClause
    updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs
    -- 'with' won't happen, include for completeness
    updateRHS (WithClause fc lhs wval prf flags cs) rhs
      = WithClause fc lhs wval prf flags cs
    updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs

    dropLams : Nat -> RawImp -> RawImp
    dropLams Z tm = tm
    dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
    dropLams _ tm = tm

splittableNames : RawImp -> List Name
splittableNames (IApp _ f (IBindVar _ n))
    = splittableNames f ++ [UN $ Basic n]
splittableNames (IApp _ f _)
    = splittableNames f
splittableNames (IAutoApp _ f _)
    = splittableNames f
splittableNames (INamedApp _ f _ _)
    = splittableNames f
splittableNames _ = []

trySplit : {auto m : Ref MD Metadata} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           FC -> RawImp -> ClosedTerm -> RawImp -> Name ->
           Core (Name, List ImpClause)
trySplit loc lhsraw lhs rhs n
    = do OK updates <- getSplitsLHS loc 0 lhs n
            | _ => pure (n, [])
         pure (n, map (\ups => PatClause loc (updateLHS ups lhsraw) rhs)
                      (mapMaybe valid updates))
  where
    valid : ClauseUpdate -> Maybe (List (Name, RawImp))
    valid (Valid lhs' ups) = Just ups
    valid _ = Nothing

    fixNames : RawImp -> RawImp
    fixNames (IVar loc' (UN (Basic n))) = IBindVar loc' n
    fixNames (IVar loc' (MN _ _)) = Implicit loc' True
    fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a)
    fixNames (IAutoApp loc' f a) = IAutoApp loc' (fixNames f) (fixNames a)
    fixNames (INamedApp loc' f t a) = INamedApp loc' (fixNames f) t (fixNames a)
    fixNames tm = tm

    updateLHS : List (Name, RawImp) -> RawImp -> RawImp
    updateLHS ups (IVar loc' n)
        = case lookup n ups of
               Nothing => IVar loc' n
               Just tm => fixNames tm
    updateLHS ups (IBindVar loc' n)
        = case lookup (UN (Basic n)) ups of
               Nothing => IBindVar loc' n
               Just tm => fixNames tm
    updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a)
    updateLHS ups (IAutoApp loc' f a) = IAutoApp loc' (updateLHS ups f) (updateLHS ups a)
    updateLHS ups (INamedApp loc' f t a)
        = INamedApp loc' (updateLHS ups f) t (updateLHS ups a)
    updateLHS ups tm = tm

generateSplits : {auto m : Ref MD Metadata} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 FC -> SearchOpts -> Int -> ImpClause ->
                 Core (List (Name, List ImpClause))
generateSplits loc opts fn (ImpossibleClause fc lhs) = pure []
generateSplits loc opts fn (WithClause fc lhs wval prf flags cs) = pure []
generateSplits loc opts fn (PatClause fc lhs rhs)
    = do (lhstm, _) <-
                elabTerm fn (InLHS linear) [] (MkNested []) []
                         (IBindHere loc PATTERN lhs) Nothing
         let splitnames =
                 if ltor opts then splittableNames lhs
                              else reverse (splittableNames lhs)
         traverse (trySplit fc lhs lhstm rhs) splitnames

collectClauses : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 List (Search (List ImpClause)) ->
                 Core (Search (List ImpClause))
collectClauses [] = one []
collectClauses (x :: xs)
    = do xs' <- collectClauses xs
         combine (++) x xs'

mutual
  tryAllSplits : {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 FC -> SearchOpts -> Int ->
                 List (Name, List ImpClause) ->
                 Core (Search (List ImpClause))
  tryAllSplits loc opts n [] = noResult
  tryAllSplits loc opts n ((x, []) :: rest)
      = tryAllSplits loc opts n rest
  tryAllSplits loc opts n ((x, cs) :: rest)
      = do log "interaction.generate" 5 $ "Splitting on " ++ show x
           trySearch (do cs' <- traverse (mkSplits loc opts n) cs
                         collectClauses cs')
                     (tryAllSplits loc opts n rest)

  mkSplits : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> SearchOpts -> Int -> ImpClause ->
             Core (Search (List ImpClause))
  -- If the clause works, use it. Otherwise, split on one of the splittable
  -- variables and try all of the resulting clauses
  mkSplits loc opts n c
      = trySearch
          (if mustSplit opts
              then noResult
              else expandClause loc opts n c)
          (do cs <- generateSplits loc opts n c
              log "interaction.generate" 5 $ "Splits: " ++ show cs
              tryAllSplits loc (record { mustSplit = False,
                                         doneSplit = True } opts) n cs)

export
makeDefFromType : {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
                  {auto u : Ref UST UState} ->
                  FC ->
                  SearchOpts ->
                  Name -> -- function name to generate
                  Nat -> -- number of arguments
                  ClosedTerm -> -- type of function
                  Core (Search (FC, List ImpClause))
makeDefFromType loc opts n envlen ty
    = tryUnify
         (do defs <- branch
             meta <- get MD
             ust <- get UST
             argns <- getEnvArgNames defs envlen !(nf defs [] ty)
             -- Need to add implicit patterns for the outer environment.
             -- We won't try splitting on these
             let pre_env = replicate envlen (Implicit loc True)

             rhshole <- uniqueName defs [] (fnName False n ++ "_rhs")
             let initcs = PatClause loc
                                (apply (IVar loc n) (pre_env ++ (map (IBindVar loc) argns)))
                                (IHole loc rhshole)
             let Just nidx = getNameID n (gamma defs)
                 | Nothing => undefinedName loc n
             cs' <- mkSplits loc opts nidx initcs
             -- restore the global state, given that we've fiddled with it a lot!
             put Ctxt defs
             put MD meta
             put UST ust
             pure (map (\c => (loc, c)) cs'))
         noResult

export
makeDef : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
          Name -> Core (Search (FC, List ImpClause))
makeDef p n
    = do Just (loc, nidx, envlen, ty) <- findTyDeclAt p
            | Nothing => noResult
         n <- getFullName nidx
         logTerm "interaction.generate" 5 ("Searching for " ++ show n) ty
         let opts = record { genExpr = Just (makeDefFromType (justFC loc)) }
                           (initSearchOpts True 5)
         makeDefFromType (justFC loc) opts n envlen ty

-- Given a clause, return the bindable names, and the ones that were used in
-- the rhs
bindableUsed : ImpClause -> Maybe (List Name, List Name)
bindableUsed (PatClause fc lhs rhs)
    = let lhsns = findIBindVars lhs
          rhsns = findAllNames [] rhs in
          Just (lhsns, filter (\x => x `elem` lhsns) rhsns)
bindableUsed _ = Nothing

propBindableUsed : List ImpClause -> Double
propBindableUsed def
    = let (b, u) = getProp def in
          if b == Z
             then 1.0
             else the Double (cast u) / the Double (cast b)
  where
    getProp : List ImpClause -> (Nat, Nat)
    getProp [] = (0, 0)
    getProp (c :: xs)
        = let (b, u) = getProp xs in
              case bindableUsed c of
                   Nothing => (b, u)
                   Just (b', u') => (b + length (nub b'), u + length (nub u'))

-- Sort by highest proportion of bound variables used. This recalculates every
-- time it looks, which might seem expensive, but it's only inspecting (not
-- constructing anything) and it would make the code ugly if we avoid that.
-- Let's see if it's a bottleneck before doing anything about it...
export
mostUsed : List ImpClause -> List ImpClause -> Ordering
mostUsed def1 def2 = compare (propBindableUsed def2) (propBindableUsed def1)

export
makeDefSort : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
              Nat -> (List ImpClause -> List ImpClause -> Ordering) ->
              Name -> Core (Search (FC, List ImpClause))
makeDefSort p max ord n
    = searchSort max (makeDef p n) (\x, y => ord (snd x) (snd y))

export
makeDefN : {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
           Nat -> Name -> Core (List (FC, List ImpClause))
makeDefN p max n
    = do (res, _) <- searchN max (makeDef p n)
         pure res


text:
module Commons.Options.ArgParse.Parser.API

import Data.String.Views

import Text.Token
import Text.Lexer
import Text.Parser

import Commons.Options.ArgParse.Lexer
import public Commons.Text.Parser.Support

%default total
%access export

-- Some basic parsers used by all the intermediate forms

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

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

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

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

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

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

ext: idr

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Mrk.MimeTypes

%default total
%access public export

data TextSubtype
  = Plain
  | CSS

Show TextSubtype where
  show Plain = "plain"
  show CSS = "css"

data MimeType
  = Text TextSubtype

Show MimeType where
  show (Text subType) = "text/" ++ show subType

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
a : Integer
a = 3+4

b : Integer
b = 7

some_proposition : Bool
some_proposition = 4+7==11

another_proposition : Bool
another_proposition = 3+8==11

complicated : Bool
complicated = 4+5*3-7==13-1

p : Bool
p = 8>5

q : Bool
q = "Hello" == "Goodbye"

r : Bool
r = True

j : Integer
j = 9001

u : Bool
u = ("Hello" == "Goodbye") || (3==3)

s : String
s = ifThenElse (3==3) "tick" "tock"

max_stars_repo_name: Nikolaj-K/idris

max_issues_repo_name: Nikolaj-K/idris

max_forks_repo_name: Nikolaj-K/idris


text:
import BasicTypes

%access public export
mutual

    -- vim : set ts=2 sw=2 et :
    record FileDescriptorSet where
      constructor MkFileDescriptorSet
      file : List FileDescriptorProto

    record FileDescriptorProto where
      constructor MkFileDescriptorProto
      name : Maybe String
      package : Maybe String
      dependency : List String
      publicDependency : List Int32
      weakDependency : List Int32
      recordType : List DescriptorProto
      enumType : List EnumDescriptorProto
      service : List ServiceDescriptorProto
      extension : List FieldDescriptorProto
      options : Maybe FileOptions
      sourceCodeInfo : Maybe SourceCodeInfo
      syntax_ : Maybe String

    namespace DescriptorProto
      record ExtensionRange where
        constructor MkExtensionRange
        start : Maybe Int32
        end : Maybe Int32
      record ReservedRange where
        constructor MkReservedRange
        start : Maybe Int32
        end : Maybe Int32

    record DescriptorProto where
      constructor MkDescriptorProto
      name : Maybe String
      field : List FieldDescriptorProto
      extension : List FieldDescriptorProto
      nestedType : List DescriptorProto
      enumType : List EnumDescriptorProto

      extensionRange : List ExtensionRange
      oneofDecl : List OneofDescriptorProto
      options : Maybe MessageOptions

      reservedRange : List ReservedRange
      reservedName : List String

    namespace FieldDescriptorProto
      Type_ : Type
      Type_ = Int
      namespace Type_
        DOUBLE         : Type_
        FLOAT          : Type_
        INT64          : Type_
        UINT64         : Type_
        INT32          : Type_
        FIXED64        : Type_
        FIXED32        : Type_
        BOOL           : Type_
        STRING         : Type_
        GROUP          : Type_
        MESSAGE        : Type_
        BYTES          : Type_
        UINT32         : Type_
        ENUM           : Type_
        SFIXED32       : Type_
        SFIXED64       : Type_
        SINT32         : Type_
        SINT64         : Type_
        DOUBLE         = 1
        FLOAT          = 2
        INT64          = 3
        UINT64         = 4
        INT32          = 5
        FIXED64        = 6
        FIXED32        = 7
        BOOL           = 8
        STRING         = 9
        GROUP          = 10
        MESSAGE        = 11
        BYTES          = 12
        UINT32         = 13
        ENUM           = 14
        SFIXED32       = 15
        SFIXED64       = 16
        SINT32         = 17
        SINT64         = 18
      Label : Type
      Label = Int
      namespace Label
        OPTIONAL      : Label
        REQUIRED      : Label
        REPEATED      : Label
        OPTIONAL      = 1
        REQUIRED      = 2
        REPEATED      = 3
    record FieldDescriptorProto where
      constructor MkFieldDescriptorProto
      name : Maybe String
      number : Maybe Int32
      label : Maybe Label
      type : Maybe Type
      typeName : Maybe String
      extendee : Maybe String
      defaultValue : Maybe String
      oneofIndex : Maybe Int32
      jsonName : Maybe String
      options : Maybe FieldOptions

    record OneofDescriptorProto where
      constructor MkOneofDescriptorProto
      name : Maybe String
      options : Maybe OneofOptions

    record EnumDescriptorProto where
      constructor MkEnumDescriptorProto
      name : Maybe String
      value : List EnumValueDescriptorProto
      options : Maybe EnumOptions

    record EnumValueDescriptorProto where
      constructor MkEnumValueDescriptorProto
      name : Maybe String
      number : Maybe Int32
      options : Maybe EnumValueOptions

    record ServiceDescriptorProto where
      constructor MkServiceDescriptorProto
      name : Maybe String
      method : List MethodDescriptorProto
      options : Maybe ServiceOptions

    record MethodDescriptorProto where
      constructor MkMethodDescriptorProto
      name : Maybe String
      inputType : Maybe String
      outputType : Maybe String
      options : Maybe MethodOptions
      clientStreaming : Maybe Bool
      serverStreaming : Maybe Bool

    namespace FileOptions
        OptimizeMode : Type
        OptimizeMode = Int

        SPEED : OptimizeMode
        CODE_SIZE : OptimizeMode
        LITE_RUNTIME : OptimizeMode
        SPEED = 1
        CODE_SIZE = 2
        LITE_RUNTIME = 3
    record FileOptions where
      constructor MkFileOptions
      javaPackage : Maybe String
      javaOuterClassname : Maybe String
      javaMultipleFiles : Maybe Bool
      javaGenerateEqualsAndHash : Maybe Bool
      javaStringCheckUtf8 : Maybe Bool

      optimizeFor : Maybe OptimizeMode
      goPackage : Maybe String
      ccGenericServices : Maybe Bool
      javaGenericServices : Maybe Bool
      pyGenericServices : Maybe Bool
      phpGenericServices : Maybe Bool
      deprecated : Maybe Bool
      ccEnableArenas : Maybe Bool
      objcClassPrefix : Maybe String
      csharpNamespace : Maybe String
      swiftPrefix : Maybe String
      phpClassPrefix : Maybe String
      phpNamespace : Maybe String
      uninterpretedOption : List UninterpretedOption

    record MessageOptions where
      constructor MkMessageOptions
      recordSetWireFormat : Maybe Bool
      noStandardDescriptorAccessor : Maybe Bool
      deprecated : Maybe Bool
      mapEntry : Maybe Bool
      uninterpretedOption : List UninterpretedOption

    namespace FieldOptions
        CType : Type
        CType = Int

        STRING : CType
        CORD : CType
        STRING_PIECE : CType
        STRING = 0
        CORD = 1
        STRING_PIECE = 2

        JSType : Type
        JSType = Int
        JS_NORMAL : JSType
        JS_STRING : JSType
        JS_NUMBER : JSType
        JS_NORMAL = 0
        JS_STRING = 1
        JS_NUMBER = 2

    record FieldOptions where
      constructor MkFieldOptions
      ctype : Maybe CType

      packed : Maybe Bool
      jstype : Maybe JSType

      lazy : Maybe Bool
      deprecated : Maybe Bool
      weak : Maybe Bool
      uninterpretedOption : List UninterpretedOption

    record OneofOptions where
      constructor MkOneofOptions
      uninterpretedOption : List UninterpretedOption

    record EnumOptions where
      constructor MkEnumOptions
      allowAlias : Maybe Bool
      deprecated : Maybe Bool
      uninterpretedOption : List UninterpretedOption

    record EnumValueOptions where
      constructor MkEnumValueOptions
      deprecated : Maybe Bool
      uninterpretedOption : List UninterpretedOption

    record ServiceOptions where
      constructor MkServiceOptions
      deprecated : Maybe Bool
      uninterpretedOption : List UninterpretedOption

    namespace MethodOptions
        IdempotencyLevel : Type
        IdempotencyLevel = Int

        IDEMPOTENCY_UNKNOWN : IdempotencyLevel
        NO_SIDE_EFFECTS     : IdempotencyLevel
        IDEMPOTENT          : IdempotencyLevel
        IDEMPOTENCY_UNKNOWN = 0
        NO_SIDE_EFFECTS     = 1
        IDEMPOTENT          = 2

    record MethodOptions where
      constructor MkMethodOptions
      deprecated : Maybe Bool

      idempotencyLevel : Maybe IdempotencyLevel
      uninterpretedOption : List UninterpretedOption

    namespace UninterpretedOption
      record NamePart where
        constructor MkNamePart
        namePart : String
        isExtension : Bool

    record UninterpretedOption where
      constructor MkUninterpretedOption
      name : List NamePart
      identifierValue : Maybe String
      positiveIntValue : Maybe Bits64
      negativeIntValue : Maybe Int64
      DoubleValue : Maybe Double
      StringValue : Maybe Bytes
      aggregateValue : Maybe String

    namespace SourceCodeInfo
      record Location where
        constructor MkLocation
        path : List Int32
        span : List Int32
        leadingComments : Maybe String
        trailingComments : Maybe String
        leadingDetachedComments : List String
    record SourceCodeInfo where
      constructor MkSourceCodeInfo
      location : List Location

    namespace GeneratedCodeInfo
      record Annotation where
        constructor MkAnnotation
        path : List Int32
        sourceFile : Maybe String
        begin : Maybe Int32
        end : Maybe Int32
    record GeneratedCodeInfo where
      constructor MkGeneratedCodeInfo
      annotation : List Annotation

max_stars_repo_name: zenhack/idris-protobufs

max_issues_repo_name: zenhack/idris-protobufs

max_forks_repo_name: zenhack/idris-protobufs


text:
module Data.Union

%default total

||| Proof that a value is present in a list. This is
||| isomorphic to `Data.List.Elem` but with (in my opinion)
||| more fitting names for our use case.
public export
data Has : (v : a) -> (ts : List a) -> Type where
  Z : Has v (v :: vs)
  S : Has v vs -> Has v (w :: vs)

Uninhabited (Has v []) where
  uninhabited Z impossible
  uninhabited (S _) impossible

||| Removes an element from a list. This is used to
||| calculate the list of effects after a single effect
||| was properly handled.
public export
0 (-) : (ts : List a) -> (v : a) -> (prf : Has v ts) => List a
(-) (_ :: vs)      _ {prf = Z}   = vs
(-) (y :: x :: xs) v {prf = S k} = y :: (-) (x :: xs) v

||| A list of effect handlers handling effects of types `fs`
||| wrapping results in type `m`.
public export
data Handler : (fs : List (Type -> Type)) -> (m : Type -> Type) -> Type where
  Nil : Handler [] m
  (::) : (h : forall x . f x -> m x) -> Handler fs m -> Handler (f :: fs) m

||| Sum type holding a value of type `t` wrapped in one of the
||| effect types listed in `fs`.
public export
data Union : (fs : List (Type -> Type)) -> (t : Type) -> Type where
  U : (ix : Has f fs) -> (val : f t) -> Union fs t

public export
Uninhabited (Union [] t) where
  uninhabited (U ix v) = absurd ix

||| Inject an effectful computation into a `Union`.
public export %inline
inj : (prf : Has f fs) => f t -> Union fs t
inj = U prf

||| Tries to extract an effect from a `Union`.
public export
prj : (prf : Has f fs) => Union fs t -> Maybe (f t)
prj {prf = Z}    (U Z v)     = Just v
prj {prf = S ix} (U (S x) v) = prj {prf = ix} (U x v)
prj _                        = Nothing

||| Extracts the last effect from a unary sum.
public export
prj1 : Union [f] t -> f t
prj1 (U Z val) = val
prj1 (U (S x) val) impossible

||| Handles all remaining effects via the given
||| (heterogeneous) list of event handlers.
public export
handleAll : Handler fs m -> Union fs t -> m t
handleAll []       y              = absurd y
handleAll (h :: t) (U Z val)     = h val
handleAll (h :: t) (U (S y) val) = handleAll t (U y val)

||| Prepend a new effect to an existing `Union` value.
export
weaken : Union fs a -> Union (f :: fs) a
weaken (U ix val) = U (S ix) val

||| Handle on of the effects in a `Union`. Unlike in other
||| effect libraries, it's not necessary that the effect
||| is the first in the list. To improve type inference,
||| the return type is calculated from the `prf` value.
public export
decomp :  (prf : Has f fs)
       => Union fs a
       -> Either (Union (fs - f) a) (f a)
decomp {prf = Z}                      (U Z     val) = Right $ val
decomp {prf = Z}                      (U (S x) val) = Left $ U x val
decomp {prf = S y} {fs = f :: h :: t} (U Z val)     = Left $ U Z val
decomp {prf = S y} {fs = f :: h :: t} (U (S x) val) =
  mapFst weaken $ decomp (U x val)

||| Handle one of the effects in a `Union`. Unlike in other
||| effect libraries, it's not necessary that the effect
||| is the first in the list. To improve type inference,
||| the return type is calculated from the `prf` value.
public export
handle :  (prf : Has f fs)
       => (f a -> res)
       -> Union fs a
       -> Either (Union (fs - f) a) res
handle g = map g . decomp


text:
||| Borrowed From Idris2 and improved with Test.Unit
module Netlist

import Data.List

import Test.Golden

%default total

dump : TestPool
dump
  = MkTestPool "Dump"
        []
        Nothing
        [
          "netlist-common-good"
        ]

tests : TestPool
tests
  = MkTestPool "Tests"
        []
        Nothing
        [
          "netlist-linear-good-001"
        , "netlist-linear-good-002"

        , "netlist-linear-bad-001"
        , "netlist-linear-bad-002"

        , "netlist-datatype-001"
        ]

covering
main : IO ()
main
  = runner [ tests, dump ]

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Prelude.Types

import Builtin
import PrimIO
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Interfaces
import Prelude.Num
import Prelude.Uninhabited

%default total

-----------
-- NATS ---
-----------

||| Natural numbers: unbounded, unsigned integers which can be pattern matched.
public export
data Nat =
  ||| Zero.
    Z
  | ||| Successor.
  S Nat

%name Nat k, j, i

public export
integerToNat : Integer -> Nat
integerToNat x
  = if intToBool (prim__lte_Integer x 0)
       then Z
       else S (assert_total (integerToNat (prim__sub_Integer x 1)))

-- Define separately so we can spot the name when optimising Nats
||| Add two natural numbers.
||| @ x the number to case-split on
||| @ y the other numberpublic export
public export
plus : (1 x : Nat) -> (1 y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y)

||| Subtract natural numbers.  If the second number is larger than the first,
||| return 0.
public export
minus : (1 left : Nat) -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

||| Multiply natural numbers.
public export
mult : (1 x : Nat) -> Nat -> Nat
mult Z y = Z
mult (S k) y = plus y (mult k y)

public export
Num Nat where
  (+) = plus
  (*) = mult

  fromInteger x = integerToNat x

public export
Eq Nat where
  Z == Z = True
  S j == S k = j == k
  _ == _ = False

public export
Ord Nat where
  compare Z Z = EQ
  compare Z (S k) = LT
  compare (S k) Z = GT
  compare (S j) (S k) = compare j k

public export
natToInteger : Nat -> Integer
natToInteger Z = 0
natToInteger (S k) = 1 + natToInteger k
                         -- integer (+) may be non-linear in second
                         -- argument

-----------
-- PAIRS --
-----------

public export
Functor (Pair a) where
  map f (x, y) = (x, f y)

public export
mapFst : (a -> c) -> (a, b) -> (c, b)
mapFst f (x, y) = (f x, y)

-----------
-- MAYBE --
-----------

||| An optional value.  This can be used to represent the possibility of
||| failure, where a function may return a value, or not.
public export
data Maybe : (ty : Type) -> Type where
  ||| No value stored
  Nothing : Maybe ty

  ||| A value of type `ty` is stored
  Just : (1 x : ty) -> Maybe ty

public export
Uninhabited (Nothing = Just x) where
  uninhabited Refl impossible

public export
Uninhabited (Just x = Nothing) where
  uninhabited Refl impossible

public export
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
maybe n j Nothing  = n
maybe n j (Just x) = j x

public export
Eq a => Eq (Maybe a) where
  Nothing  == Nothing  = True
  Nothing  == (Just _) = False
  (Just _) == Nothing  = False
  (Just a) == (Just b) = a == b

public export
Ord a => Ord (Maybe a) where
  compare Nothing  Nothing  = EQ
  compare Nothing  (Just _) = LT
  compare (Just _) Nothing  = GT
  compare (Just a) (Just b) = compare a b

public export
Semigroup (Maybe a) where
  Nothing   <+> m = m
  (Just x)  <+> _ = Just x

public export
Monoid (Maybe a) where
  neutral = Nothing

public export
Functor Maybe where
  map f (Just x) = Just (f x)
  map f Nothing  = Nothing

public export
Applicative Maybe where
  pure = Just

  Just f <*> Just a = Just (f a)
  _      <*> _        = Nothing

public export
Alternative Maybe where
    empty = Nothing

    (Just x) <|> _ = Just x
    Nothing  <|> v = v

public export
Monad Maybe where
  Nothing  >>= k = Nothing
  (Just x) >>= k = k x

public export
Foldable Maybe where
  foldr _ z Nothing  = z
  foldr f z (Just x) = f x z

public export
Traversable Maybe where
  traverse f Nothing = pure Nothing
  traverse f (Just x) = (pure Just) <*> (f x)

---------
-- DEC --
---------

||| Decidability.  A decidable property either holds or is a contradiction.
public export
data Dec : Type -> Type where
  ||| The case where the property holds.
  ||| @ prf the proof
  Yes : (prf : prop) -> Dec prop

  ||| The case where the property holding would be a contradiction.
  ||| @ contra a demonstration that prop would be a contradiction
  No  : (contra : prop -> Void) -> Dec prop

------------
-- EITHER --
------------

||| A sum type.
public export
data Either : (a : Type) -> (b : Type) -> Type where
  ||| One possibility of the sum, conventionally used to represent errors.
  Left : forall a, b. (1 x : a) -> Either a b

  ||| The other possibility, conventionally used to represent success.
  Right : forall a, b. (1 x : b) -> Either a b

||| Simply-typed eliminator for Either.
||| @ f the action to take on Left
||| @ g the action to take on Right
||| @ e the sum to analyze
public export
either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c
either l r (Left x) = l x
either l r (Right x) = r x

public export
(Eq a, Eq b) => Eq (Either a b) where
  Left x == Left x' = x == x'
  Right x == Right x' = x == x'
  _ == _ = False

public export
(Ord a, Ord b) => Ord (Either a b) where
  compare (Left x) (Left x') = compare x x'
  compare (Left _) (Right _) = LT
  compare (Right _) (Left _) = GT
  compare (Right x) (Right x') = compare x x'

%inline
public export
Functor (Either e) where
  map f (Left x) = Left x
  map f (Right x) = Right (f x)

%inline
public export
Applicative (Either e) where
    pure = Right

    (Left a) <*> _          = Left a
    (Right f) <*> (Right r) = Right (f r)
    (Right _) <*> (Left l)  = Left l

public export
Monad (Either e) where
    (Left n) >>= _ = Left n
    (Right r) >>= f = f r

public export
Foldable (Either e) where
  foldr f acc (Left _) = acc
  foldr f acc (Right x) = f x acc

public export
Traversable (Either e) where
  traverse f (Left x)  = pure (Left x)
  traverse f (Right x) = Right <$> f x

-----------
-- LISTS --
-----------

||| Generic lists.
public export
data List a =
  ||| Empty list
  Nil

  | ||| A non-empty list, consisting of a head element and the rest of the list.
  (::) a (List a)

%name List xs, ys, zs

public export
Eq a => Eq (List a) where
  [] == [] = True
  x :: xs == y :: ys = x == y && xs == ys
  _ == _ = False

public export
Ord a => Ord (List a) where
  compare [] [] = EQ
  compare [] (x :: xs) = LT
  compare (x :: xs) [] = GT
  compare (x :: xs) (y ::ys)
     = case compare x y of
            EQ => compare xs ys
            c => c

namespace List
  public export
  (++) : (1 xs, ys : List a) -> List a
  [] ++ ys = ys
  (x :: xs) ++ ys = x :: xs ++ ys

  public export
  length : List a -> Nat
  length []        = Z
  length (x :: xs) = S (length xs)

public export
Functor List where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

public export
Semigroup (List a) where
  (<+>) = (++)

public export
Monoid (List a) where
  neutral = []

public export
Foldable List where
  foldr c n [] = n
  foldr c n (x::xs) = c x (foldr c n xs)

  foldl f q [] = q
  foldl f q (x::xs) = foldl f (f q x) xs

public export
Applicative List where
  pure x = [x]
  fs <*> vs = concatMap (\f => map f vs) fs

public export
Alternative List where
    empty = []
    (<|>) = (++)

public export
Monad List where
  m >>= f = concatMap f m

public export
Traversable List where
  traverse f [] = pure []
  traverse f (x::xs) = pure (::) <*> (f x) <*> (traverse f xs)

||| Check if something is a member of a list using the default Boolean equality.
public export
elem : Eq a => a -> List a -> Bool
x `elem` [] = False
x `elem` (y :: ys) = x == y ||  elem x ys

-------------
-- STREAMS --
-------------

namespace Stream
  ||| An infinite stream.
  public export
  data Stream : Type -> Type where
       (::) : a -> Inf (Stream a) -> Stream a

public export
Functor Stream where
  map f (x :: xs) = f x :: map f xs

||| The first element of an infinite stream.
public export
head : Stream a -> a
head (x :: xs) = x

||| All but the first element.
public export
tail : Stream a -> Stream a
tail (x :: xs) = xs

||| Take precisely n elements from the stream.
||| @ n how many elements to take
||| @ xs the stream
public export
take : (1 n : Nat) -> (xs : Stream a) -> List a
take Z xs = []
take (S k) (x :: xs) = x :: take k xs

-------------
-- STRINGS --
-------------

namespace Strings
  public export
  (++) : (1 x : String) -> (1 y : String) -> String
  x ++ y = prim__strAppend x y

  ||| Returns the length of the string.
  |||
  ||| ```idris example
  ||| length ""
  ||| ```
  ||| ```idris example
  ||| length "ABC"
  ||| ```
  public export
  length : String -> Nat
  length str = fromInteger (prim__cast_IntInteger (prim__strLength str))

||| Reverses the elements within a string.
|||
||| ```idris example
||| reverse "ABC"
||| ```
||| ```idris example
||| reverse ""
||| ```
public export
reverse : String -> String
reverse = prim__strReverse

||| Returns a substring of a given string
|||
||| @ index The (zero based) index of the string to extract.  If this is beyond
|||         the end of the string, the function returns the empty string.
||| @ len The desired length of the substring.  Truncated if this exceeds the
|||       length of the input
||| @ subject The string to return a portion of
public export
substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String
substr s e subj
    = if natToInteger s < natToInteger (length subj)
         then prim__strSubstr (prim__cast_IntegerInt (natToInteger s))
                              (prim__cast_IntegerInt (natToInteger e))
                              subj
         else ""

||| Adds a character to the front of the specified string.
|||
||| ```idris example
||| strCons 'A' "B"
||| ```
||| ```idris example
||| strCons 'A' ""
||| ```
public export
strCons : Char -> String -> String
strCons = prim__strCons

public export
strUncons : String -> Maybe (Char, String)
strUncons "" = Nothing
strUncons str = assert_total $ Just (prim__strHead str, prim__strTail str)

||| Turns a list of characters into a string.
public export
pack : List Char -> String
pack [] = ""
pack (x :: xs) = strCons x (pack xs)

%foreign
    "scheme:string-pack"
    "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
export
fastPack : List Char -> String

||| Turns a string into a list of characters.
|||
||| ```idris example
||| unpack "ABC"
||| ```
public export
unpack : String -> List Char
unpack str =
  case strUncons str of
    Nothing => []
    Just (x, xs) => x :: unpack (assert_smaller str xs)

public export
Semigroup String where
  (<+>) = (++)

public export
Monoid String where
  neutral = ""

----------------
-- CHARACTERS --
----------------

||| Returns true if the character is in the range [A-Z].
public export
isUpper : Char -> Bool
isUpper x = x >= 'A' && x <= 'Z'

||| Returns true if the character is in the range [a-z].
public export
isLower : Char -> Bool
isLower x = x >= 'a' && x <= 'z'

||| Returns true if the character is in the ranges [A-Z][a-z].
public export
isAlpha : Char -> Bool
isAlpha x = isUpper x || isLower x

||| Returns true if the character is in the range [0-9].
public export
isDigit : Char -> Bool
isDigit x = (x >= '0' && x <= '9')

||| Returns true if the character is in the ranges [A-Z][a-z][0-9].
public export
isAlphaNum : Char -> Bool
isAlphaNum x = isDigit x || isAlpha x

||| Returns true if the character is a whitespace character.
public export
isSpace : Char -> Bool
isSpace x
    = x == ' '  || x == '\t' || x == '\r' ||
      x == '\n' || x == '\f' || x == '\v' ||
      x == '\xa0'

||| Returns true if the character represents a new line.
public export
isNL : Char -> Bool
isNL x = x == '\r' || x == '\n'

||| Convert a letter to the corresponding upper-case letter, if any.
||| Non-letters are ignored.
public export
toUpper : Char -> Char
toUpper x
    = if (isLower x)
         then prim__cast_IntChar (prim__cast_CharInt x - 32)
         else x

||| Convert a letter to the corresponding lower-case letter, if any.
||| Non-letters are ignored.
public export
toLower : Char -> Char
toLower x
    = if (isUpper x)
         then prim__cast_IntChar (prim__cast_CharInt x + 32)
         else x

||| Returns true if the character is a hexadecimal digit i.e. in the range
||| [0-9][a-f][A-F].
public export
isHexDigit : Char -> Bool
isHexDigit x = elem (toUpper x) hexChars where
  hexChars : List Char
  hexChars
      = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
         'A', 'B', 'C', 'D', 'E', 'F']

||| Returns true if the character is an octal digit.
public export
isOctDigit : Char -> Bool
isOctDigit x = (x >= '0' && x <= '7')

||| Returns true if the character is a control character.
public export
isControl : Char -> Bool
isControl x
    = (x >= '\x0000' && x <= '\x001f')
       || (x >= '\x007f' && x <= '\x009f')

||| Convert the number to its backend dependent (usually Unicode) Char
||| equivalent.
public export
chr : Int -> Char
chr = prim__cast_IntChar

||| Return the backend dependent (usually Unicode) numerical equivalent of the Char.
public export
ord : Char -> Int
ord = prim__cast_CharInt

-----------------------
-- DOUBLE PRIMITIVES --
-----------------------

public export
pi : Double
pi = 3.14159265358979323846

public export
euler : Double
euler = 2.7182818284590452354

public export
exp : Double -> Double
exp x = prim__doubleExp x

public export
log : Double -> Double
log x = prim__doubleLog x

public export
pow : Double -> Double -> Double
pow x y = exp (y * log x)

public export
sin : Double -> Double
sin x = prim__doubleSin x

public export
cos : Double -> Double
cos x = prim__doubleCos x

public export
tan : Double -> Double
tan x = prim__doubleTan x

public export
asin : Double -> Double
asin x = prim__doubleASin x

public export
acos : Double -> Double
acos x = prim__doubleACos x

public export
atan : Double -> Double
atan x = prim__doubleATan x

public export
sinh : Double -> Double
sinh x = (exp x - exp (-x)) / 2

public export
cosh : Double -> Double
cosh x = (exp x + exp (-x)) / 2

public export
tanh : Double -> Double
tanh x = sinh x / cosh x

public export
sqrt : Double -> Double
sqrt x = prim__doubleSqrt x

public export
floor : Double -> Double
floor x = prim__doubleFloor x

public export
ceiling : Double -> Double
ceiling x = prim__doubleCeiling x

-----------
-- CASTS --
-----------

-- Casts between primitives only here.  They might be lossy.

||| Interface for transforming an instance of a data type to another type.
public export
interface Cast from to where
  ||| Perform a (potentially lossy!) cast operation.
  ||| @ orig The original type
  cast : (orig : from) -> to

-- To String

export
Cast Int String where
  cast = prim__cast_IntString

export
Cast Integer String where
  cast = prim__cast_IntegerString

export
Cast Char String where
  cast = prim__cast_CharString

export
Cast Double String where
  cast = prim__cast_DoubleString

-- To Integer

export
Cast Int Integer where
  cast = prim__cast_IntInteger

export
Cast Char Integer where
  cast = prim__cast_CharInteger

export
Cast Double Integer where
  cast = prim__cast_DoubleInteger

export
Cast String Integer where
  cast = prim__cast_StringInteger

export
Cast Nat Integer where
  cast = natToInteger

export
Cast Bits8 Integer where
  cast = prim__cast_Bits8Integer

export
Cast Bits16 Integer where
  cast = prim__cast_Bits16Integer

export
Cast Bits32 Integer where
  cast = prim__cast_Bits32Integer

export
Cast Bits64 Integer where
  cast = prim__cast_Bits64Integer

-- To Int

export
Cast Integer Int where
  cast = prim__cast_IntegerInt

export
Cast Char Int where
  cast = prim__cast_CharInt

export
Cast Double Int where
  cast = prim__cast_DoubleInt

export
Cast String Int where
  cast = prim__cast_StringInt

export
Cast Nat Int where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int where
  cast = prim__cast_Bits8Int

export
Cast Bits16 Int where
  cast = prim__cast_Bits16Int

export
Cast Bits32 Int where
  cast = prim__cast_Bits32Int

export
Cast Bits64 Int where
  cast = prim__cast_Bits64Int

-- To Char

export
Cast Int Char where
  cast = prim__cast_IntChar

-- To Double

export
Cast Int Double where
  cast = prim__cast_IntDouble

export
Cast Integer Double where
  cast = prim__cast_IntegerDouble

export
Cast String Double where
  cast = prim__cast_StringDouble

export
Cast Nat Double where
  cast = prim__cast_IntegerDouble . natToInteger

-- To Bits8

export
Cast Int Bits8 where
  cast = prim__cast_IntBits8

export
Cast Integer Bits8 where
  cast = prim__cast_IntegerBits8

export
Cast Bits16 Bits8 where
  cast = prim__cast_Bits16Bits8

export
Cast Bits32 Bits8 where
  cast = prim__cast_Bits32Bits8

export
Cast Bits64 Bits8 where
  cast = prim__cast_Bits64Bits8

-- To Bits16

export
Cast Int Bits16 where
  cast = prim__cast_IntBits16

export
Cast Integer Bits16 where
  cast = prim__cast_IntegerBits16

export
Cast Bits8 Bits16 where
  cast = prim__cast_Bits8Bits16

export
Cast Bits32 Bits16 where
  cast = prim__cast_Bits32Bits16

export
Cast Bits64 Bits16 where
  cast = prim__cast_Bits64Bits16

-- To Bits32

export
Cast Int Bits32 where
  cast = prim__cast_IntBits32

export
Cast Integer Bits32 where
  cast = prim__cast_IntegerBits32

export
Cast Bits8 Bits32 where
  cast = prim__cast_Bits8Bits32

export
Cast Bits16 Bits32 where
  cast = prim__cast_Bits16Bits32

export
Cast Bits64 Bits32 where
  cast = prim__cast_Bits64Bits32

-- To Bits64

export
Cast Int Bits64 where
  cast = prim__cast_IntBits64

export
Cast Integer Bits64 where
  cast = prim__cast_IntegerBits64

export
Cast Bits8 Bits64 where
  cast = prim__cast_Bits8Bits64

export
Cast Bits16 Bits64 where
  cast = prim__cast_Bits16Bits64

export
Cast Bits32 Bits64 where
  cast = prim__cast_Bits32Bits64

------------
-- RANGES --
------------

public export
countFrom : n -> (n -> n) -> Stream n
countFrom start diff = start :: countFrom (diff start) diff

-- this and takeBefore are for range syntax, and not exported here since
-- they're partial. They are exported from Data.Stream instead.
partial
takeUntil : (n -> Bool) -> Stream n -> List n
takeUntil p (x :: xs)
    = if p x
         then [x]
         else x :: takeUntil p xs

partial
takeBefore : (n -> Bool) -> Stream n -> List n
takeBefore p (x :: xs)
    = if p x
         then []
         else x :: takeBefore p xs

public export
interface Range a where
  rangeFromTo : a -> a -> List a
  rangeFromThenTo : a -> a -> a -> List a

  rangeFrom : a -> Stream a
  rangeFromThen : a -> a -> Stream a

-- Idris 1 went to great lengths to prove that these were total. I don't really
-- think it's worth going to those lengths! Let's keep it simple and assert.
export
Range Nat where
  rangeFromTo x y
      = if y > x
           then assert_total $ takeUntil (>= y) (countFrom x S)
           else if x > y
                   then assert_total $ takeUntil (<= y) (countFrom x (\n => minus n 1))
                   else [x]
  rangeFromThenTo x y z
      = if y > x
           then (if z > x
                    then assert_total $ takeBefore (> z) (countFrom x (plus (minus y x)))
                    else [])
           else (if x == y
                    then (if x == z then [x] else [])
                    else assert_total $ takeBefore (< z) (countFrom x (\n => minus n (minus x y))))
  rangeFrom x = countFrom x S
  rangeFromThen x y
      = if y > x
           then countFrom x (plus (minus y x))
           else countFrom x (\n => minus n (minus x y))

export
(Integral a, Ord a, Neg a) => Range a where
  rangeFromTo x y
      = if y > x
           then assert_total $ takeUntil (>= y) (countFrom x (+1))
           else if x > y
                   then assert_total $ takeUntil (<= y) (countFrom x (\x => x-1))
                   else [x]
  rangeFromThenTo x y z
      = if (z - x) > (z - y)
           then -- go up
             assert_total $ takeBefore (> z) (countFrom x (+ (y-x)))
           else if (z - x) < (z - y)
                then -- go down
                     assert_total $ takeBefore (< z) (countFrom x (\n => n - (x - y)))
                else -- meaningless
                  if x == y && y == z
                     then [x] else []
  rangeFrom x = countFrom x (1+)
  rangeFromThen x y
      = if y > x
           then countFrom x (+ (y - x))
           else countFrom x (\n => n - (x - y))


text:
module Data.Nat.Views

import Control.WellFounded
import Data.Nat

%default total

||| View for dividing a Nat in half
public export
data Half : Nat -> Type where
     HalfOdd : (n : Nat) -> Half (S (n + n))
     HalfEven : (n : Nat) -> Half (n + n)

||| View for dividing a Nat in half, recursively
public export
data HalfRec : Nat -> Type where
     HalfRecZ : HalfRec Z
     HalfRecEven : (n : Nat) -> (rec : Lazy (HalfRec n)) -> HalfRec (n + n)
     HalfRecOdd : (n : Nat) -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))

||| Covering function for the `Half` view
public export
half : (n : Nat) -> Half n
half Z = HalfEven Z
half (S k) with (half k)
  half (S (S (n + n))) | HalfOdd n = rewrite plusSuccRightSucc (S n) n in
                                           HalfEven (S n)
  half (S (n + n)) | HalfEven n = HalfOdd n

public export
halfRec : (n : Nat) -> HalfRec n
halfRec n with (sizeAccessible n)
  halfRec  Z | acc = HalfRecZ
  halfRec (S n) | acc with (half n)
    halfRec (S (S (k + k))) | Access acc | HalfOdd k
      = rewrite plusSuccRightSucc (S k) k
          in HalfRecEven _ (halfRec (S k) | acc (S k) (LTESucc (LTESucc (lteAddRight _))))
    halfRec (S (k + k)) | Access acc | HalfEven k
      = HalfRecOdd _ (halfRec k | acc k (LTESucc (lteAddRight _)))


text:
||| Module that provides fixed-point number to represent seconds in nanoseconds.
module Fixed

public export
data Fixed a = MkFixed Integer

public export
data E12
data E9
data E2

public export
Dec : Type
Dec = Fixed E2

public export
Pico : Type
Pico = Fixed E12

public export
Nano : Type
Nano = Fixed E9

public export
Show (Fixed a) where
  show (MkFixed x) = show x

export
Eq (Fixed a) where
  (MkFixed a) == (MkFixed b) = a == b

export
Ord (Fixed a) where
  compare (MkFixed a) (MkFixed b) = compare a b

export
interface HasResolution (a: Type) where
  resolution : (f : Type -> Type) -> f a -> Integer

export
HasResolution E12 where
  resolution _ _ =  1000000000000

export
HasResolution E2 where
  resolution _ _ =  100

public export
Enum (Fixed a) where
  pred (MkFixed x) = MkFixed (pred x)
  toNat (MkFixed x) = toNat x
  fromNat x = MkFixed (toIntegerNat x)

-- Currently unable to express `*` in terms of `div` due to totality checking
-- implementation (HasResolution a) => Num (Fixed a) where
--   (+) (MkFixed x) (MkFixed y) = MkFixed (x + y)
--   (*) fa@(MkFixed x) (MkFixed y)  = MkFixed (div (x * y) (resolution {a} Fixed fa))
--   fromInteger x = MkFixed x

export
add: Fixed a -> Fixed a -> Fixed a
add (MkFixed x) (MkFixed y) = MkFixed (x + y)

export
(+) : Fixed a -> Fixed a -> Fixed a
(+) = add

export
sub : Fixed a -> Fixed a -> Fixed a
sub (MkFixed x) (MkFixed y) = MkFixed (x - y)

export
(-) : Fixed a -> Fixed a -> Fixed a
(-) = sub

export
negate: Fixed a -> Fixed a
negate (MkFixed x) = MkFixed (negate x)

export
abs : Fixed a -> Fixed a
abs (MkFixed x) = MkFixed (abs x)

export
fromInteger : Integer -> Fixed a
fromInteger x = MkFixed x

export
toRational : (HasResolution a) => Fixed a -> Double
toRational {a} fa@(MkFixed x) = (cast x) / cast (resolution {a} Fixed fa)

export
multFixed : (HasResolution a) => Fixed a -> Fixed a -> Fixed a
multFixed {a} fa@(MkFixed x) (MkFixed y) =
  let
    result =  div (x * y) (resolution {a} Fixed fa)
  in
    MkFixed result

--MkFixed (x * y  * cast (1 / (resolution {a} Fixed fa)))

export
(*) : (HasResolution a) => Fixed a -> Fixed a -> Fixed a
(*) = multFixed

export
fracDiv : (HasResolution a) => Fixed a -> Fixed a -> Fixed a
fracDiv fa@(MkFixed x) (MkFixed y) = MkFixed (div (x * (resolution {a} Fixed fa)) y)

export
(/): (HasResolution a) => Fixed a -> Fixed a -> Fixed a
(/) = fracDiv

export
recip : (HasResolution a) => Fixed a -> Fixed a
recip {a} fa@(MkFixed x) = MkFixed (div ((resolution {a} Fixed fa) * (resolution {a} Fixed fa)) x)

-- TODO:
-- fromRationalFixed:

-- implementation (HasResolution a) => Num (Fixed a) where
--   (+) (MkFixed x) (MkFixed y) = addFixed
--   (*) fa@(MkFixed x) (MkFixed y)  = MkFixed (x * y * (resolution {a} Fixed fa))
--   fromInteger x = MkFixed x

--(HasResolution a) => Fractional (Fixed a) where
--  (/) = fraceDivFixed
--   --recip fa@(MkFixed x) =

--   -- MkFixed (div (res * res) x)
--   --                        where
--   --                        res = (resolution {a} Fixed fa)

-- partial
-- implementation (HasResolution a) => Integral (Fixed a) where
--   div (MkFixed x) (MkFixed y) = MkFixed (div x y)
--   mod (MkFixed x) (MkFixed y) = MkFixed (mod x y)

  --fromRational r = withResolution (\res -> MkFixed (floor (r * (toRational res))))

  -- (MkFixed a) + (MkFixed b) = MkFixed (a + b)
  -- (MkFixed a) - (MkFixed b) = MkFixed (a - b)
  -- fa@(MkFixed a) * (MkFixed b) = MkFixed (div (a * b) (resolution fa))
  -- negate (MkFixed a) = MkFixed (negate a)
  -- abs (MkFixed a) = MkFixed (abs a)
  -- signum (MkFixed a) = fromInteger (signum a)
  -- fromInteger i = withResolution (\res -> MkFixed (i * res))

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module ZZ_alt

import congruence
import Quotient_Type

%access public export
%default total

ZZ1 : Type
ZZ1 = (Nat, Nat)

ZZ_Rel : (Nat, Nat) -> (Nat, Nat) -> Type
ZZ_Rel (a, b) (c, d) = ( (plus a d) = (plus b c) )

IsRefl_ZZ_Rel : (n : ZZ1) -> (ZZ_Rel n n)
IsRefl_ZZ_Rel (a, b) = (plusCommutative a b)

IsSym_ZZ_Rel : (n, m : ZZ1) -> (ZZ_Rel n m) -> (ZZ_Rel m n)
IsSym_ZZ_Rel (a, b) (c, d) pf_rel = (rewrite (plusCommutative d a) in
                                    (rewrite (plusCommutative c b) in (sym pf_rel)))

congruence_1 : (ty1 : Type) -> (ty2 : Type) -> (a, b, c, d : ty1) ->
               (f : ty1 -> ty1 -> ty2) -> (a = b) -> (c = d) -> ( (f a c) = (f b d) )

congruence_1 ty1 ty2 a a c c f Refl Refl = Refl

succCancellation : (a, b : Nat) -> ( (S a) = (S b) ) -> (a = b)
succCancellation a a Refl = Refl

plusCancellation_left : (a, b, c : Nat) -> ( (plus c a) = (plus c b) ) -> (a = b)

plusCancellation_left a b Z pf = pf

plusCancellation_left a b (S k) pf = let

    pf1 : (plus k a = plus k b)
        = succCancellation (plus k a) (plus k b) pf
    in

    (plusCancellation_left a b k pf1)

plusCancellation_right : (a, b, c : Nat) -> ( (plus a c) = (plus b c) ) -> (a = b)

plusCancellation_right a b Z pf = (rewrite (plusCommutative Z b) in
                            (rewrite (plusCommutative Z a) in pf))

plusCancellation_right a b (S k) pf = let

    pf1 : ( plus a (S k) = S (plus k a) )
        = plusCommutative a (S k)

    pf2 : ( plus b (S k) = S (plus k b) )
        = ( plusCommutative b (S k))

    pf3 : ( S (plus k a) = S (plus k b) )
        = trans (sym pf1) (trans pf pf2)
    in
    (plusCancellation_left a b (S k) pf3)

IsTrans_ZZ_Rel : (a, b, c : ZZ1) -> (ZZ_Rel a b) -> (ZZ_Rel b c) -> (ZZ_Rel a c)
IsTrans_ZZ_Rel (a, b) (c, d) (k, l) pf1 pf2 = let

    pf3 : (plus (plus a d) (plus c l) = plus (plus b c) (plus d k))
        = congruence_1 Nat Nat (plus a d) (plus b c) (plus c l) (plus d k) plus pf1 pf2

    pf4 : (plus a (plus d (plus c l)) = plus (plus a d) (plus c l))
        = plusAssociative a d (plus c l)

    pf5 : (plus b (plus c (plus d k)) = plus (plus b c) (plus d k))
        = plusAssociative b c (plus d k)

    pf6 : (plus c l = plus l c)
        = plusCommutative c l

    pf7 : (plus d (plus c l) = plus d (plus l c))
        = congruence Nat Nat (plus c l) (plus l c) (\x => (plus d x)) pf6

    pf8 : (plus d (plus l c) = plus (plus d l) c)
        = plusAssociative d l c

    pf9 : (plus d (plus c l) = plus (plus d l) c)
        = trans pf7 pf8

    pf10 : (plus d l = plus l d)
         = plusCommutative d l

    pf11 : (plus (plus d l) c = plus (plus l d) c)
         = congruence Nat Nat (plus d l) (plus l d) (\x => (plus x c)) pf10

    pf12 : ( plus d (plus l c) = plus (plus l d) c )
         = trans pf8 pf11

    pf13 : (plus d (plus c l) = plus (plus l d) c)
         = trans pf7 pf12

    pf14 : (plus l (plus d c) = plus (plus l d) c)
         = plusAssociative l d c

    pf15 : ( plus (plus d l) c = plus l (plus d c) )
         = trans pf11 (sym pf14)

    pf16 : (plus d (plus c l) = plus l (plus d c))
         = trans pf9 pf15

    pf17 : (plus a (plus d (plus c l)) = plus a (plus l (plus d c)))
         = congruence Nat Nat (plus d (plus c l)) (plus l (plus d c)) (\x => (plus a x)) pf16

    pf18 : (plus a (plus l (plus d c)) = plus (plus a l) (plus d c))
         = plusAssociative a l (plus d c)

    pf19 : (plus (plus a d) (plus c l) = plus (plus a l) (plus d c))
         = trans (trans (sym pf4) pf17) pf18

    pf20 : ( plus d k = plus k d )
         = plusCommutative d k

    pf21 : ( plus c (plus d k) = plus c (plus k d) )
         = congruence Nat Nat (plus d k) (plus k d) (\x => (plus c x)) pf20

    pf22 : ( plus c (plus k d) = plus (plus c k) d )
         = plusAssociative c k d

    pf23 : (  plus c k = plus k c )
         = plusCommutative c k

    pf24 : ( plus (plus c k) d = plus (plus k c) d )
         = congruence Nat Nat (plus c k) (plus k c) (\x => (plus x d)) pf23

    pf25 : ( plus (plus k c) d = plus k (plus c d) )
         = sym (plusAssociative k c d)

    pf26 : ( plus c (plus d k) = plus k (plus c d) )
         = trans pf21 (trans pf22 (trans pf24 pf25))

    pf27 : ( plus b (plus c (plus d k)) = plus b (plus k (plus c d)) )
         = congruence Nat Nat (plus c (plus d k)) (plus k (plus c d)) (\x => (plus b x)) pf26

    pf28 : ( plus b (plus k (plus c d)) = plus (plus b k) (plus c d) )
         = plusAssociative b k (plus c d)

    pf29 : ( plus c d = plus d c )
         = plusCommutative c d

    pf30 : ( plus (plus b k) (plus c d) = plus (plus b k) (plus d c) )
         = congruence Nat Nat (plus c d) (plus d c) (\x => (plus (plus b k) x)) pf29

    pf31 : ( plus b (plus c (plus d k)) = plus (plus b k) (plus d c) )
         = (trans (trans pf27 pf28) pf30)

    pf32 : ( plus (plus b c) (plus d k) = plus (plus b k) (plus d c) )
         = trans (sym pf5) pf31

    pf33 : ( plus (plus a l) (plus d c) = plus (plus b k) (plus d c) )
         = trans (trans (sym pf19) pf3) pf32

    in
    (plusCancellation_right (plus a l) (plus b k) (plus d c) pf33)

ZZ_Rel_is_EqRel : IsEqRel ZZ1 ZZ_Rel
ZZ_Rel_is_EqRel = (IsRefl_ZZ_Rel, (IsSym_ZZ_Rel, IsTrans_ZZ_Rel))

ZZ_Quotient : (Quotient_Type ZZ1 ZZ_Rel)
ZZ_Quotient = Cons_quotient_Type ZZ_Rel_is_EqRel


text:
module Toolkit.Options.ArgParse.Parser.API

import Data.List
import Data.String

import Text.Token
import Text.Lexer
import Text.Parser

import Toolkit.Options.ArgParse.Lexer
import public Toolkit.Text.Parser.Support

%default total

namespace ArgParse
  public export
  Rule : Type -> Type
  Rule = Rule Unit Token

  public export
  RuleEmpty : Type -> Type
  RuleEmpty = RuleEmpty Unit Token

-- Some basic parsers used by all the intermediate forms

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

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

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

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

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

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

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
||| A MonadRef instance with heap and locations indexed by a universe.
|||
||| Note:
||| - We can't make an instance `MonadRef (Loc es) (RefT es es' m)`
|||   because `Loc es : Ty u -> Type` instead of `Type -> Type`...
module Experiment.TypedHeap

import public Experiment.RefUniverseConstraint

%default total
%access public export

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

-- Implementation --------------------------------------------------------------

-- Types --

||| The shape of a heap.
|||
||| Determines the type of data stored at every memory location.
||| Heaps have a length `k` and every location has a certain type `t` from the universe `u`.
Shape : {u : Universe t} -> Type
Shape {t} = List t

||| Hetrogenious heap indexed by a `Shape`.
|||
||| `Nil` is the empty heap.
||| `(::)` allocates a value `a` of type `typeOf e` on a heap `as` of shape `es`
||| to construct a heap of shape `e :: es`.
|||
||| Note: corresponds to an universe indexed variant of `Data.HVect`.
data Heap : {u : Universe t} -> (es : Shape {u}) -> Type where
  Nil  : Heap []
  (::) : (a : typeOf @{u} e) -> (as : Heap {u} es) -> Heap {u} (e :: es)

||| Location on the heap.
|||
||| A value of type `Loc es e` corresponds to a proof that a value of type `typeOf e`
||| is stored in a heap of shape `es`.
||| `Here` means it is stored at this location.
||| `There` means it is stored a bit further on the heap.
|||
||| Note: corresponds to an universe indexed variant of `Data.Vect.Elem`.
data Loc : {u : Universe t} -> (es : Shape {u}) -> (e : t) -> Type where
  Here  : Loc (e :: es) e
  There : (later : Loc {u} es e) -> Loc {u} (e' :: es) e

data RefT : {u : Universe t} -> (es : Shape {u}) -> (es' : Shape {u}) -> (m : Type -> Type) -> (a : Type) -> Type where
  Pure  : (x : a) -> RefT es es m a
  Bind  : (this : RefT {u} es es' m a) -> (next : a -> RefT {u} es' es'' m b) -> RefT {u} es es'' m b

  New   : (x : typeOf @{u} e) -> RefT {u} es (e :: es) m (Loc {u} (e :: es) e)
  Read  : (l : Loc {u} es e) -> RefT {u} es es m (typeOf @{u} e)
  Write : (l : Loc {u} es e) -> (x : typeOf @{u} e) -> RefT {u} es es m ()

Ref : {u : Universe t} -> (es : Shape {u}) -> (es' : Shape {u}) -> (a : Type) -> Type
Ref {u} es es' = RefT {u} es es' Identity

-- Semantics --

lookup : (u : Universe t) => Loc es e -> Heap es -> typeOf @{u} e
lookup _         []        impossible
lookup (Here)    (x :: _)  = ?h
-- lookup (There l) (_ :: xs) = lookup l xs

{-------------------------------------------------------------------------------

update : Loc es e -> typeOf @{u} e -> Heap es -> Heap es
update _         _ []        impossible
update (Here)    y (_ :: xs) = y :: xs
update (There l) y (x :: xs) = x :: update l y xs

runT : Monad m => RefT es es' m a -> Heap es -> m ( a, Heap es' )
runT (Pure x)         xs = pure ( x, xs )
runT (Bind this next) xs = do
  ( this, xs' ) <- runT this xs
  runT (next this) xs'
runT (New x)          xs = pure ( Here, x :: xs )
runT (Read l)         xs = pure ( lookup l xs, xs )
runT (Write l x)      xs = pure ( (), update l x xs )

run : Ref es es' a -> Heap es -> ( a, Heap es' )
run r = runIdentity . runT r

eval : Ref es es' a -> Heap es -> a
eval mut = fst . run mut

exec : Ref es es' a -> Heap es -> Heap es'
exec mut = snd . run mut

-- Instances -------------------------------------------------------------------

Functor f => Functor (RefT es es' f) where
  map f fa = ?holeFunctor

Applicative f => Applicative (RefT es es' f) where
  pure a = ?holePureApplicative

  f <*> fa = ?holeApplyApplicative

Monad m => Monad (RefT es es' m) where
  fa >>= f = ?holeMonadBind

Monad m => MonadRef u (Loc es) (RefT es es' m) where
  ref x = ?holeMonadRefRef
  deref l = ?holeMonadRefDeref
  assign l x = ?holeMonadRefAssign

-------------------------------------------------------------------------------}

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module LightClick.Env

import Data.List
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect
import Toolkit.Data.DList.DeBruijn
import Toolkit.Data.Location
import Toolkit.Data.Rig
import Toolkit.Decidable.Equality.Indexed

import Language.SystemVerilog.Utilities

import LightClick.Connection
import LightClick.Error

import LightClick.Types
import LightClick.Types.Equality
import LightClick.Types.Usage
import LightClick.Terms

import LightClick.Values

%default total

namespace TheType

   public export
   data TheType : (String, MTy) -> Type where
     MkTheType : (s : String) -> Ty ty -> TheType (s,ty)

   public export
   Equals : {a,b : Pair String MTy}
         -> (x : TheType a)
         -> (y : TheType b)
              -> Type
   Equals = Equals (String,MTy) TheType

   typesDiffer : (Types.Equality.Equals tyA tyB -> Void)
              -> TheType.Equals (MkTheType l tyA) (MkTheType l tyB)
              -> Void
   typesDiffer contra (Same Refl Refl) = contra (Same Refl Refl)

   decEq : (x : TheType a)
        -> (y : TheType b)
        -> (prf : a = b)
        -> Dec (Equals x y)
   decEq (MkTheType l tyA) (MkTheType l tyB) Refl with (decEq tyA tyB Refl)
     decEq (MkTheType l tyA) (MkTheType l tyA) Refl | Yes (Same Refl Refl) = Yes (Same Refl Refl)
     decEq (MkTheType l tyA) (MkTheType l tyB) Refl | No contra = No (typesDiffer contra)

   export
   DecEqIdx (String, MTy) TheType where
     decEq = TheType.decEq

public export
data Entry : Pair String MTy -> Type where
  MkEntry : (value : Value (interp ty))
         -> (type  : TheType (s,ty))
                 -> Entry (s,ty)

public export
Env : Context -> Type
Env = DeBruijn.Env (Pair String MTy) Entry

export
free : Env context -> List (Pair String (List String))
free [] = Nil
free ((MkEntry value (MkTheType name type)) :: rest) with (free type)
  free ((MkEntry value (MkTheType name type)) :: rest) | []
    = free rest
  free ((MkEntry value (MkTheType name type)) :: rest) | (x :: xs)
    = (name,x::xs) :: free rest

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
-- ----------------------------------------------------------- [ Chapter10.idr ]
-- Module      : Exercises.Chapter10
-- Description : Solutions to the Chapter 10 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.Chapter10

import Data.List.Views
import Data.Nat.Views
import Data.Vect
import Data.Vect.Views
import Test

%access  export
%default total

---------------------------------------------------------- [ Exercise 10.1.6.1 ]

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

takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN _ [] = Fewer
takeN Z _  = Exact []
takeN (S Z) (x :: xs) = Exact [x]
takeN (S k) (x :: xs) with (takeN k xs)
  takeN (S k) (x :: xs) | Fewer = Fewer
  takeN (S k) (x :: (n_xs ++ rest)) | (Exact n_xs) = Exact (x :: n_xs)

-- partial
groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN Z _ = [[]]           -- Provide a sensible base case.
groupByN n xs with (takeN n xs)
 groupByN n  xs            | Fewer      = [xs]
 -- HACK: Assert to the totality checker that groupByN will always terminate.
 groupByN n (n_xs ++ rest) | Exact n_xs = n_xs :: assert_total (groupByN n rest)
 -- groupByN n (n_xs ++ rest) | Exact n_xs = n_xs :: groupByN n rest

---------------------------------------------------------- [ Exercise 10.1.6.2 ]

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

---------------------------------------------------------- [ Exercise 10.2.5.1 ]

{- NOTE: Here's isSuffix for reference. It's quite similar to equalSuffix.
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
  isSuffix [] input2 | Empty = True
  isSuffix (xs ++ [x]) input2 | (Snoc rec) with (snocList input2)
    isSuffix (xs ++ [x]) [] | (Snoc rec) | Empty = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
      x == y && isSuffix xs ys | xsrec | ysrec
-}

-- FIXME: I don't love this. It would be great to accumulate a SnocList then
-- convert it to a list at the end, though maybe that's no different from
-- accumulating a singly linked list and then reversing it.
equalSuffixHelp : Eq a => (acc, input1, input2 : List a) -> List a
equalSuffixHelp acc input1 input2 with (snocList input1)
  equalSuffixHelp acc [] input2 | Empty = []
  equalSuffixHelp acc (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    equalSuffixHelp acc (xs ++ [x]) [] | (Snoc xsrec) | Empty = []
    equalSuffixHelp acc (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
      if x /= y then [] else x :: equalSuffixHelp acc xs ys | xsrec | ysrec

equalSuffix : Eq a => (input1, input2 : List a) -> List a
equalSuffix input1 input2 = reverse $ equalSuffixHelp [] input1 input2

---------------------------------------------------------- [ Exercise 10.2.5.2 ]

mergeSort : Ord a => Vect n a -> Vect n a
mergeSort xs with (splitRec xs)
  mergeSort []                | SplitRecNil = []
  mergeSort [x]               | SplitRecOne = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) =
    merge (mergeSort lefts  | lrec)
          (mergeSort rights | rrec)

---------------------------------------------------------- [ Exercise 10.2.5.3 ]

-- FIXME: This is ineffecient due to the string appending, at least.
toBinary : (n : Nat) -> String
toBinary n with (halfRec n)
  toBinary  Z          |  HalfRecZ         = ""
  toBinary (x + x)     | (HalfRecEven rec) = (toBinary x | rec) ++ "0"
  toBinary (S (x + x)) | (HalfRecOdd  rec) = (toBinary x | rec) ++ "1"

---------------------------------------------------------- [ Exercise 10.2.5.4 ]

palindrome : Eq a => (xs : List a) -> Bool
palindrome xs with (vList xs)
  palindrome []  | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (ys ++ [y])) | (VCons rec) = x == y && palindrome ys | rec

---------------------------------------------------------------------- [ Tests ]

-- partial
testGroupByN : IO ()
testGroupByN = assertEq [[1,2,3],[4,5,6],[7,8,9],[10]] $
                        the (List (List Integer)) (groupByN 3 [1..10])

partial
testHalves10 : IO ()
testHalves10 = assertEq ([1..5], [6..10]) $ halves [1..10]

partial
testHalves1 : IO ()
testHalves1 = assertEq ([], [1]) $ the (List Integer, List Integer) (halves [1])

testEqualSuffix1 : IO ()
testEqualSuffix1 = assertEq (the (List Integer) [4,5])
                            (equalSuffix [1,2,4,5] [1..5])

testEqualSuffix2 : IO ()
testEqualSuffix2 = assertEq [] $ equalSuffix [1,2,4,5,6] [1..5]

testEqualSuffix3 : IO ()
testEqualSuffix3 = assertEq (the (List Integer) [4,5,6])
                            (equalSuffix [1,2,4,5,6] [1..6])

testMergeSort1 : IO ()
testMergeSort1 = assertEq (fromList [1,2,3]) (mergeSort [3,2,1])

testMergeSort2 : IO ()
testMergeSort2 = assertEq (fromList [1..9]) (mergeSort [5,1,4,3,2,6,8,7,9])

testToBinary42 : IO ()
testToBinary42 = assertEq "101010" $ toBinary 42

testToBinary94 : IO ()
testToBinary94 = assertEq "1011110" $ toBinary 94

testToBinaryExercism : IO ()
testToBinaryExercism =
  assertEq (the (List String) ["1", "10", "11", "100", "1001", "11010"])
           (map toBinary [1,2,3,4,9,26])

testPalindrome1 : IO ()
testPalindrome1 = assertEq True $ palindrome (unpack "abccba")

testPalindrome2 : IO ()
testPalindrome2 = assertEq True $ palindrome (unpack "abcba")

testPalindrome3 : IO ()
testPalindrome3 = assertEq False $ palindrome (unpack "abcb")

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
%default partial

foo : Maybe a -> a
foo (Just x) = x

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

data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

lookup : Fin n -> Vect n a -> a
lookup FZ (x :: xs) = x
lookup (FS k) (x :: xs) = lookup k xs

lookup' : Fin n -> Vect n a -> a
lookup' (FS k) (x :: xs) = lookup' k xs

lookup'' : Fin n -> Vect n a -> a
lookup'' n xs = lookup' n xs

main : IO ()
main = do let x = foo Nothing
          printLn (the Int x)


text:
data DumbNumber = Naught | One | Two | Three
data Natural = Zero | After Natural
data MyList a = Blank | (::) a (MyList a)

data MMaybe a = Nothing | Just a

first : MyList a -> MMaybe a
first Blank = Nothing
first (x :: xs) = Just x

filterGreaterThan : Integer -> List Integer -> List Integer
filterGreaterThan n list = filter (\x => x > n) list

everyOtherElement : List a -> List a
everyOtherElement [] = []
everyOtherElement (x :: xs) = x :: (everyOtherElement (drop 1 xs))

reverseList : List a -> List a
reverseList [] = []
reverseList (x :: xs) = (reverseList xs) ++ [x]

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

max_stars_repo_name: dkandalov/katas

max_issues_repo_name: dkandalov/katas

max_forks_repo_name: dkandalov/katas


text:
module LinearAlgebra

import BaseN
import Linear.MultiSolver
import Data.Matrix.Numeric
import Data.Vect
import Data.Fin
import Merge
import Data.Matrix
import ZZ
import Rationals

%access public export

-- Some auxillary functions for elementary operations

FST: ZZPair -> ZZ --some issue with fst
FST (a, b) = a

Pred: Nat -> Nat -- needed to get (n-1) for number of operations
Pred Z = Z
Pred (S k) = k

SimpleCast:  (v1:(Vect (k+ (S Z)) elem)) ->( Vect (S k) elem)  -- necessary for type matching, taken from Shafil's code
SimpleCast {k} v1 = (Vecttake (S k) v1)

RowN: Matrix n n ZZPair -> (k: Nat) -> Vect n ZZPair -- returns the nth row (indexing from 0)
RowN {n} x k = Data.Vect.index (tofinNat k n) x

ij: Matrix n n ZZPair -> (i: Nat) -> (j: Nat) -> ZZPair
ij {n} x i j = Data.Vect.index (tofinNat j n) (RowN x i)

ColumnN: Matrix n n ZZPair -> (k: Nat) -> Vect n ZZPair --returns the nth column (indexing from 0)
ColumnN {n} x k = Data.Vect.index (tofinNat k n) (transpose x)

VectorSubtract: (n: Nat) -> (a: Vect n ZZPair) -> (b: Vect n ZZPair) -> (Vect n ZZPair) --subtracts components
VectorSubtract n a b = a - b

ScaleVect: (n: Nat) -> (Vect n ZZPair) -> (c: ZZPair) -> (Vect n ZZPair) --scales by a rational
ScaleVect n xs c = c <# xs

--returns the row scaled by a constant minus another vector (used in row operations)

axpy: (n: Nat) -> (a: Vect n ZZPair) -> (b: Vect n ZZPair) -> (c: ZZPair) -> (Vect n ZZPair)
axpy n a b c = VectorSubtract (n) (a) (ScaleVect (n) b c)

--Auxillary functions, will be used in the Gauss-Jordan process

First_k_rows: (n: Nat) -> (x: Matrix n n ZZPair) -> (k: Nat) -> Matrix k n ZZPair
First_k_rows n x Z = []
First_k_rows n x (S k) = [RowN x k] ++ (First_k_rows n x k)

Last_k_rows: (n: Nat) -> (x: Matrix n n ZZPair) -> (k: Nat) -> Matrix k n ZZPair
Last_k_rows n x k = reverse (First_k_rows n (reverse x) k)

First_k_rows_from_RowP: (n: Nat) -> (x: Matrix n n ZZPair) -> (p: Nat) -> (k: Nat) -> Matrix k n ZZPair
First_k_rows_from_RowP n x p Z = []
First_k_rows_from_RowP n x p (S k) = SimpleCast ((First_k_rows_from_RowP n x p k) ++ [RowN x (p+k)])

-- A section on elementary operations (to eventually implement the Gauss-Jordan process)

-- Swaps two rows in a matrix (indexing from 0)

SwapRows: (n: Nat) -> Matrix n n ZZPair -> (a: Nat) -> (b: Nat) -> Matrix n n ZZPair
SwapRows n x a b = replaceAt (tofinNat b n) (RowN x a) (replaceAt (tofinNat a n) (RowN x b) (x))

-- Performs an elementary row operation, subtracts from row a the row b scaled by c

RowOperation: (n: Nat) -> Matrix n n ZZPair -> (a: Nat) -> (b: Nat) -> (c: ZZPair) -> Matrix n n ZZPair
RowOperation n x a b c = replaceAt (tofinNat a n) (axpy n (RowN x a) (RowN x b) c) (x)

-- Makes the kth number in Row A zero by subtracting a scaling of Row B (for upper triangularizing)
-- As usual, indexing starts from 0

MakeElementZero: (n: Nat) -> (x: Matrix n n ZZPair) -> (row_a : Nat) -> (row_b : Nat) -> (pos : Nat) -> Matrix n n ZZPair
MakeElementZero n x row_a row_b pos = case (FST(ij x row_a pos)) of
                                      (Pos Z) => x
                                      (Pos (S k)) => case ((fst (ij x row_b pos))) of
                                                                          (Pos Z) => (SwapRows n x row_a row_b)
                                                                          (Pos (S k)) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )
                                                                          (NegS k) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )
                                      (NegS k) => case ((fst (ij x row_b pos))) of
                                                                          (Pos Z) => (SwapRows n x row_a row_b)
                                                                          (Pos (S k)) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )
                                                                          (NegS k) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )

-- Explanation: We want to transform the element x[row_a][pos] into zero by a row operation. There are a few different cases
--              1. If x[row_a][pos] is already zero, nothing needs to be done.
--              2. If not, we scale row_b appropriately and do a row operation (A -> A - cB)
--              3. If x[row_b][pos] is zero, however, no row operation will work. We simply swap the
--                 row_a and row_b here; then, x[row_a][pos] will become zero.

-- This algorithm is important to make a matrix upper-triangular.

MakeColumnZero: (n: Nat) -> (x: Matrix n n ZZPair) -> (col : Nat) -> (iter : Nat) -> Matrix n n ZZPair
MakeColumnZero n x col Z = x
MakeColumnZero n x col (S k) = case (isLTE (S k) col) of
                                   (Yes prf) => x
                                   (No contra) => (MakeColumnZero n (MakeElementZero n x (S k) col col) col k)

-- This function turns a column into what it should be in upper-triangular form by adding in the necessary zeros.
-- iter is a variable to induct on (trick courtesy Sriram)
-- When using this, make sure to set "iter" as n-1 (1 less than the number of rows)

-- The next step here is to use the above function to make a matrix upper triangular. This can be
-- done by inducting on the number of columns.

-- A helper function, which recursively fills zeros into columns.

UpperTriangularize: (x: Matrix n n ZZPair) -> (iter: Nat) -> Matrix n n ZZPair
UpperTriangularize {n} x Z = (MakeColumnZero n x Z (Pred n)) -- Column Zero is the base case
UpperTriangularize {n} x (S k) = (MakeColumnZero n (UpperTriangularize x k) (S k) (Pred n))

-- Enter a matrix, get the upper triangular form.

UpperTriangularForm: (x: Matrix n n ZZPair) -> Matrix n n ZZPair
UpperTriangularForm {n} x = UpperTriangularize x (Pred (Pred n))

-- The function below converts a matrix into a Diagonal Form (note that this is NOT diagonalization!) by converting to upper-triangular
-- form, transposing that (to get a lower triangular matrix) and finding the upper-triangular form of the tranpose. This is going to be useful
-- as it is the next step of the Gauss-Jordan algorithm (what's next: divide out the rows to get an identity matrix; an inverse can be
-- found this way by applying all the above row operations to an identity matrix.

DiagonalForm: (x: Matrix n n ZZPair) -> Matrix n n ZZPair
DiagonalForm {n} x = UpperTriangularForm (transpose (UpperTriangularForm x))


text:
namespace MyDo
  export
  (>>=) : a -> (a -> IO b) -> IO b
  (>>=) val k = k val

foo : IO ()
foo = MyDo.do
         x <- "Silly"
         putStrLn x


text:
module Idrlisp.Parser

import Text.Parser
import Idrlisp.Sexp
import Idrlisp.Lexer

%default total

public export
interface Parse (c : Bool) (ty : Type) | ty where
  grammar : Grammar Token c ty

export
parseToEnd : Parse c ty => String -> Either String ty
parseToEnd {c} {ty} input =
  case lex input of
    Left (line, col, _) =>
      Left $ "Parse error at " ++ show line ++ ":" ++ show col ++ ": lexical error"
    Right tokens =>
      -- If we place parseToEnd in interface, grammar reports that the implementation is missing
      case parse (grammar {c} {ty} <* eof) tokens of
        Left (Error msg _) => Left $ "Parse error: " ++ msg
        Right (x, _) => Right x

namespace Terminal
  term : Token -> Grammar Token True ()
  term t = terminal $ \t' => toMaybe (t == t') ()

  num : Grammar Token True Double
  num = terminal $ \t =>
    case t of
      NUM x => Just x
      _ => Nothing

  sym : Grammar Token True String
  sym = terminal $ \t =>
    case t of
      SYM x => Just x
      _ => Nothing

  str : Grammar Token True String
  str = terminal $ \t =>
    case t of
      STR x => Just x
      _ => Nothing

mutual
  s : Grammar Token True (SSyn a)
  s = choice
    [ list LPAREN RPAREN
    , list LBRACK RBRACK
    , quotes
    , Num <$> num
    , Sym <$> sym
    , Str <$> str
    , do term TRUE; pure $ Bool True
    , do term FALSE; pure $ Bool False
    ]

  quotes : Grammar Token True (SSyn a)
  quotes =
    do
      f <- quote
      commit
      x <- s
      pure $ f x
    where
      -- TODO: Why these function liftings are required for the totality checker?
      quote : Grammar Token True (SSyn a -> SSyn a)
      quote = choice
        [ do term QUOTE; pure Quote
        , do term QUASIQUOTE; pure Quasiquote
        , do term UNQUOTE; pure Unquote
        , do term UNQUOTE_SPLICING; pure UnquoteSplicing
        ]

  list : Token -> Token -> Grammar Token True (SSyn a)
  list open close =
    do
      term open
      commit
      xs <- init
      y <- rest xs
      term close
      pure $ build xs y
    where
      -- TODO: ditto
      init : Grammar Token False (List (SSyn a))
      init = many s

      rest : List (SSyn a) -> Grammar Token False (Maybe (SSyn a))
      rest [] = pure Nothing
      rest _ = optional $ do term DOT; commit; s

      build : List (SSyn a) -> Maybe (SSyn a) -> SSyn a
      build [] _ = Nil
      -- TODO: Why these aren't total?
      build (x :: xs) Nothing = assert_total $ App (x :: xs)
      build (x :: xs) (Just y) = assert_total $ x :: xs :.: y

export
Parse True ty => Parse False (List ty) where
  grammar {ty} = many $ grammar {ty}

export
Parse True (SSyn a) where
  grammar = s

export
Parse True (Sexp a) where
  grammar = map cast $ grammar {ty = SSyn a}

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp