text:
module GRIN.AST

import Data.SortedMap

||| A bound variable or function argument.
public export
data Var : Type where
    MkVar : Int -> Var

export
incVar : Var -> Var
incVar (MkVar x) = MkVar (x + 1)

export
Eq Var where
    MkVar x == MkVar y = x == y

export
Ord Var where
    MkVar x `compare` MkVar y = x `compare` y

||| A type of a tag.
public export
data TagType : Type where
    ||| Data constructor.
    Con : TagType
    ||| Updating thunk.
    UThunk : TagType
    ||| Non-updating thunk.
    NUThunk : TagType
    ||| Partially applied function.
    Partial : Nat -> TagType

tagTypeToNat : TagType -> Nat
tagTypeToNat Con = 0
tagTypeToNat UThunk = 1
tagTypeToNat NUThunk = 2
tagTypeToNat (Partial k) = 3 + k

export
Eq TagType where
    (==) = (==) `on` tagTypeToNat

export
Ord TagType where
    compare = compare `on` tagTypeToNat

||| A constructor tag.
public export
record Tag name where
    constructor MkTag
    tagType : TagType
    tag : name

export
Eq name => Eq (Tag name) where
    MkTag ty1 tag1 == MkTag ty2 tag2 = ty1 == ty2 && tag1 == tag2

export
Ord name => Ord (Tag name) where
    MkTag ty1 tag1 `compare` MkTag ty2 tag2 = case compare ty1 ty2 of
        EQ => compare tag1 tag2
        o => o

export
Functor Tag where
    map f (MkTag ty tag) = MkTag ty (f tag)

export
Foldable Tag where
    foldl f z (MkTag ty tag) = f z tag
    foldr f z (MkTag ty tag) = f tag z

export
Traversable Tag where
    traverse f (MkTag ty tag) = MkTag ty <$> f tag

||| A literal value.
public export
data Lit : Type where
    LInt : Integer -> Lit
    LDouble : Double -> Lit
    LString : String -> Lit
    LChar : Char -> Lit

export
Eq Lit where
    LInt x == LInt y = x == y
    LDouble x == LDouble y = x == y
    LString x == LString y = x == y
    LChar x == LChar y = x == y
    _ == _ = False

||| The precision and signed-ness of an integer.
public export
data IntPrec : Type where
    Signed : Nat -> IntPrec
    Unsigned : Nat -> IntPrec

export
Eq IntPrec where
    Signed x == Signed y = x == y
    Unsigned x == Unsigned y = x == y
    _ == _ = False

||| Id of the store instuction a `HeapPtr` came from
public export
StoreId : Type
StoreId = Int

||| A simple type.
public export
data SType : Type where
    IntTy : IntPrec -> SType
    DoubleTy : SType
    CharTy : SType
    StringTy : SType
    UnitTy : SType
    HeapPtr : StoreId -> SType

export
Eq SType where
    IntTy x == IntTy y = x == y
    DoubleTy == DoubleTy = True
    CharTy == CharTy = True
    StringTy == StringTy = True
    UnitTy == UnitTy = True
    HeapPtr x == HeapPtr y = x == y
    _ == _ = False

||| A type of a value.
public export
data GType : (name : Type) -> Type where
    SimpleType : SType -> GType name
    TyVar : name -> GType name
    Cons : GType name -- TODO: HPT

Eq name => Eq (GType name) where
    SimpleType ty1 == SimpleType ty2 = ty1 == ty2
    Cons == Cons = True
    _ == _ = False

export
Functor GType where
    map _ (SimpleType ty) = SimpleType ty
    map f (TyVar x) = TyVar (f x)
    map _ Cons = Cons

export
Foldable GType where
    foldl f z Cons = z
    foldl f z (TyVar x) = f z x
    foldl _ z _ = z

    foldr f z Cons = z
    foldr f z (TyVar x) = f x z
    foldr _ z _ = z

export
Traversable GType where
    traverse _ (SimpleType ty) = pure (SimpleType ty)
    traverse f (TyVar x) = TyVar <$> f x
    traverse f Cons = pure Cons

||| A type of a function.
public export
record FuncType name where
    constructor MkFuncType
    args : List (GType name)
    ret : GType name

export
Eq name => Eq (FuncType name) where
    MkFuncType as1 r1 == MkFuncType as2 r2 = as1 == as2 && r1 == r2

export
Functor FuncType where
    map f (MkFuncType args ret) = MkFuncType (map (map f) args) (map f ret)

export
Foldable FuncType where
    foldl f z0 (MkFuncType args ret) =
        let z1 = foldl (foldl f) z0 args
        in foldl f z1 ret

    foldr f z0 (MkFuncType args ret) =
        let z1 = foldr f z0 ret
        in foldr (flip $ foldr f) z1 args

export
Traversable FuncType where
    traverse f (MkFuncType args ret) = [| MkFuncType (traverse (traverse f) args) (traverse f ret) |]

||| A simple value.
public export
data SVal : Type where
    SVar : Var -> SVal
    SLit : Lit -> SVal

export
Eq SVal where
    SVar x == SVar y = x == y
    SLit x == SLit y = x == y
    _ == _ = False

||| A value.
public export
data Val : (name : Type) -> Type where
    SimpleVal : SVal -> Val name
    ||| A known constructor applied to any number of arguments.
    ||| ```
    ||| pure (CInt 10)`
    ||| ```
    ConstTagNode : Tag name -> List SVal -> Val name
    ||| A known constructor applied to no arguments.
    ||| ```
    ||| pure CInt
    ||| ```
    ConstTag : Tag name -> Val name
    ||| A variable constructor applied to any number of arguments.
    ||| ```
    ||| con <- pure CInt
    ||| pure (con 10)
    ||| ```
    VarTagNode : Var -> List SVal -> Val name
    ||| Discard.
    VUnit : Val name

export
Eq name => Eq (Val name) where
    SimpleVal x == SimpleVal y = x == y
    ConstTagNode t1 vs1 == ConstTagNode t2 vs2 = vs1 == vs2 && t1 == t2
    ConstTag t1 == ConstTag t2 = t1 == t2
    VarTagNode x vs1 == VarTagNode y vs2 = x == y && vs1 == vs2
    VUnit == VUnit = True
    _ == _ = False

public export
VVar : Var -> Val name
VVar = SimpleVal . SVar

public export
VLit : Lit -> Val name
VLit = SimpleVal . SLit

export
mkCon : name -> List SVal -> Val name
mkCon con = ConstTagNode (MkTag Con con)

export
mkUThunk : name -> List SVal -> Val name
mkUThunk fn = ConstTagNode (MkTag UThunk fn)

export
mkNUThunk : name -> List SVal -> Val name
mkNUThunk fn = ConstTagNode (MkTag NUThunk fn)

export
mkPartial : name -> Nat -> List SVal -> Val name
mkPartial fn m = ConstTagNode (MkTag (Partial m) fn)

export
Functor Val where
    map _ (SimpleVal val) = SimpleVal val
    map f (ConstTagNode tag args) = ConstTagNode (map f tag) args
    map f (ConstTag tag) = ConstTag (map f tag)
    map _ (VarTagNode var args) = VarTagNode var args
    map _ VUnit = VUnit

export
Foldable Val where
    foldl f z (ConstTagNode tag _) = foldl f z tag
    foldl f z (ConstTag tag) = foldl f z tag
    foldl _ z _ = z

    foldr f z = foldl (flip f) z

export
Traversable Val where
    traverse _ (SimpleVal val) = pure $ SimpleVal val
    traverse f (ConstTagNode tag args) = (\tag' => ConstTagNode tag' args) <$> traverse f tag
    traverse f (ConstTag tag) = ConstTag <$> traverse f tag
    traverse _ (VarTagNode var args) = pure $ VarTagNode var args
    traverse _ VUnit = pure VUnit

||| Pattern on the LHS of a case alternative.
public export
data CasePat : (name : Type) -> Type where
    ||| A known constructor applied to any number of arguments.
    ||| ```
    ||| (CInt x) -> ...
    ||| ```
    NodePat : Tag name -> List Var -> CasePat name
    ||| A known constructor.
    ||| ```
    ||| CInt -> ...
    ||| ```
    TagPat : Tag name -> CasePat name
    ||| A literal.
    ||| ```
    ||| 10 -> ...
    ||| ```
    LitPat : Lit -> CasePat name
    ||| Default pattern.
    ||| ```
    ||| #default -> ...
    ||| ```
    DefaultPat : CasePat name

export
getPatTag : CasePat name -> Maybe (Tag name)
getPatTag (NodePat t _) = Just t
getPatTag (TagPat t) = Just t
getPatTag _ = Nothing

export
Eq name => Eq (CasePat name) where
    NodePat t1 as1 == NodePat t2 as2 = as1 == as2 && t1 == t2
    TagPat t1 == TagPat t2 = t1 == t2
    LitPat x == LitPat y = x == y
    DefaultPat == DefaultPat = True
    _ == _ = False

export
Functor CasePat where
    map f (NodePat tag args) = NodePat (map f tag) args
    map f (TagPat tag) = TagPat (map f tag)
    map _ (LitPat lit) = LitPat lit
    map _ DefaultPat = DefaultPat

export
Foldable CasePat where
    foldl f z (NodePat tag _) = foldl f z tag
    foldl f z (TagPat tag) = foldl f z tag
    foldl _ z _ = z

    foldr f = foldl (flip f)

export
Traversable CasePat where
    traverse f (NodePat tag args) = (\tag' => NodePat tag' args) <$> traverse f tag
    traverse f (TagPat tag) = TagPat <$> traverse f tag
    traverse _ (LitPat lit) = pure $ LitPat lit
    traverse _ DefaultPat = pure DefaultPat

mutual
    ||| A simple expression.
    public export
    data SExp : (name : Type) -> Type where
        ||| A full expression. Allows for easier inlining and phi nodes.
        Do : Exp name -> SExp name
        ||| Apply a known function to the correct number of arguments.
        App : name -> List Var -> SExp name
        ||| A value.
        Pure : Val name -> SExp name
        ||| Return a pointer to a value.
        Store : Val name -> SExp name
        ||| Fetch the value at a pointer
        Fetch : Maybe StoreId -> Var -> SExp name
        ||| Fetch a specific component of the value at a pointer.
        FetchI : Maybe StoreId -> Nat -> Var -> SExp name
        ||| Update the value at a pointer to a new value.
        Update : Var -> Val name -> SExp name

    ||| An Expression.
    public export
    data Exp : (name : Type) -> Type where
        ||| A simple value.
        SimpleExp : SExp name -> Exp name
        ||| Bind the result of a simple expression to a variable.
        Bind : Val name -> SExp name -> Exp name -> Exp name
        ||| Split to different code paths depending on provided value.
        Case : Val name -> List (Alt name) -> Exp name

    ||| A case alternative.
    public export
    data Alt : Type -> Type where
        MkAlt : CasePat name -> Exp name -> Alt name

export
altPat : Alt name -> CasePat name
altPat (MkAlt pat _) = pat

export
altExp : Alt name -> Exp name
altExp (MkAlt _ exp) = exp

export
mkDo : Exp name -> SExp name
mkDo (SimpleExp exp) = exp
mkDo exp = Do exp

export
mkSimpleExp : SExp name -> Exp name
mkSimpleExp (Do exp) = exp
mkSimpleExp exp = SimpleExp exp

export
fetch : Var -> SExp name
fetch = Fetch Nothing

export
fetchI : Nat -> Var -> SExp name
fetchI = FetchI Nothing

mutual
    export
    Eq name => Eq (SExp name) where
        Do e1 == Do e2 = e1 == e2
        App f1 as1 == App f2 as2 = as1 == as2 && f1 == f2
        Pure x == Pure y = x == y
        Store x == Store y = x == y
        Fetch i1 v1 == Fetch i2 v2 = i1 == i2 && v1 == v2
        FetchI i1 n1 v1 == FetchI i2 n2 v2 = i1 == i2 && n1 == n2 && v1 == v2
        Update x v1 == Update y v2 = x == y && v1 == v2
        _ == _ = False

    export
    Eq name => Eq (Exp name) where
        SimpleExp e1 == SimpleExp e2 = e1 == e2
        Bind v1 rhs1 rest1 == Bind v2 rhs2 rest2 = v1 == v2 && rhs1 == rhs2 && rest1 == rest2
        Case v1 alts1 == Case v2 alts2 = v1 == v2 && alts1 == alts2
        _ == _ = False

    export
    Eq name => Eq (Alt name) where
        MkAlt p1 e1 == MkAlt p2 e2 = p1 == p2 && e1 == e2

mutual
    export
    Functor SExp where
        map f (Do exp) = Do $ map f exp
        map f (App fun args) = App (f fun) args
        map f (Pure val) = Pure $ map f val
        map f (Store val) = Store $ map f val
        map _ (Fetch i var) = Fetch i var
        map _ (FetchI i idx var) = FetchI i idx var
        map f (Update var val) = Update var $ map f val

    export
    Functor Exp where
        map f (SimpleExp exp) = SimpleExp $ map f exp
        map f (Bind lhs rhs rest) = Bind (map f lhs) (map f rhs) (map f rest)
        map f (Case val alts) = Case (map f val) (map (map f) alts)

    export
    Functor Alt where
        map f (MkAlt pat exp) = MkAlt (map f pat) (map f exp)

mutual
    export
    Foldable SExp where
        foldl f z (Do exp) = foldl f z exp
        foldl f z (App fun _) = f z fun
        foldl f z (Pure val) = foldl f z val
        foldl f z (Store val) = foldl f z val
        foldl _ z (Fetch _ _) = z
        foldl _ z (FetchI _ _ _) = z
        foldl f z (Update _ val) = foldl f z val

        foldr f z (Do exp) = foldr f z exp
        foldr f z (App fun _) = f fun z
        foldr f z (Pure val) = foldr f z val
        foldr f z (Store val) = foldr f z val
        foldr _ z (Fetch _ _) = z
        foldr _ z (FetchI _ _ _) = z
        foldr f z (Update _ val) = foldr f z val

    export
    Foldable Exp where
        foldl f z (SimpleExp exp) = foldl f z exp
        foldl f z0 (Bind val rhs rest) =
            let z1 = foldl f z0 val
                z2 = foldl f z1 rhs
            in foldl f z2 rest
        foldl f z0 (Case val alts) =
            let z1 = foldl f z0 val
            in foldl (foldl f) z1 alts

        foldr f z (SimpleExp exp) = foldr f z exp
        foldr f z0 (Bind val rhs rest) =
            let z1 = foldr f z0 rest
                z2 = foldr f z1 rhs
            in foldr f z2 val
        foldr f z0 (Case val alts) =
            let z1 = foldr (flip $ foldr f) z0 alts
            in foldr f z1 val

    export
    Foldable Alt where
        foldl f z0 (MkAlt pat exp) =
            let z1 = foldl f z0 pat
            in foldl f z1 exp

        foldr f z0 (MkAlt pat exp) =
            let z1 = foldr f z0 exp
            in foldr f z1 pat

mutual
    export
    Traversable SExp where
        traverse f (Do exp) = Do <$> traverse f exp
        traverse f (App fun args) = (\fun' => App fun' args) <$> f fun
        traverse f (Pure val) = Pure <$> traverse f val
        traverse f (Store val) = Store <$> traverse f val
        traverse _ (Fetch i var) = pure $ Fetch i var
        traverse _ (FetchI i idx var) = pure $ FetchI i idx var
        traverse f (Update var val) = Update var <$> traverse f val

    export
    Traversable Exp where
        traverse f (SimpleExp exp) = SimpleExp <$> traverse f exp
        traverse f (Bind lhs rhs rest) =
            [| Bind (traverse f lhs) (traverse f rhs) (traverse f rest) |]
        traverse f (Case val alts) =
            [| Case (traverse f val) (traverse (traverse f) alts) |]

    export
    Traversable Alt where
        traverse f (MkAlt pat exp) = [| MkAlt (traverse f pat) (traverse f exp) |]

export
mapExpSExp : (Exp name -> Exp name) -> SExp name -> SExp name
mapExpSExp f (Do exp) = Do (f exp)
mapExpSExp _ exp = exp

export
mapExpAlt : (Exp name -> Exp name) -> Alt name -> Alt name
mapExpAlt f (MkAlt pat exp) = MkAlt pat (f exp)

mutual
    export
    mapSExpExp : (SExp name -> SExp name) -> Exp name -> Exp name
    mapSExpExp f (SimpleExp e) = SimpleExp (f e)
    mapSExpExp f (Bind v rhs rest) = Bind v (f rhs) (mapSExpExp f rest)
    mapSExpExp f (Case v alts) = Case v (mapSExpAlt f <$> alts)

    export
    mapSExpAlt : (SExp name -> SExp name) -> Alt name -> Alt name
    mapSExpAlt f (MkAlt pat exp) = MkAlt pat (mapSExpExp f exp)

public export
record Def name where
    constructor MkDef
    defName : name
    args : List Var
    body : Exp name
    type : Maybe (FuncType name)

export
mkDef : name -> List Var -> Exp name -> Def name
mkDef defName args body = MkDef defName args body Nothing

export
Eq name => Eq (Def name) where
    MkDef n1 as1 e1 t1 == MkDef n2 as2 e2 t2 = n1 == n2 && as1 == as2 && e1 == e2 && t1 == t2

export
Functor Def where
    map f (MkDef n as b ty) = MkDef (f n) as (map f b) (map (map f) ty)

export
Foldable Def where
    foldl f z0 (MkDef n _ b ty) =
        let z1 = f z0 n
            z2 = foldl (foldl f) z1 ty
        in foldl f z2 b
    foldr f z0 (MkDef n _ b ty) =
        let z1 = foldr f z0 b
            z2 = foldr (flip $ foldr f) z1 ty
        in f n z2

export
Traversable Def where
    traverse f (MkDef n as b ty) = [| (\n', b' => MkDef n' as b') (f n) (traverse f b) (traverse (traverse f) ty) |]

export %inline
mapExpDef : (Exp name -> Exp name) -> Def name -> Def name
mapExpDef f (MkDef n as b ty) = MkDef n as (f b) ty

public export data ExternPrim = Primop | FFI
export
Eq ExternPrim where
    Primop == Primop = True
    FFI == FFI = True
    _ == _ = False
public export data Effectful = NoEffect | Effect
export
Eq Effectful where
    NoEffect == NoEffect = True
    Effect == Effect = True
    _ == _ = False

public export
record Extern name where
    constructor MkExtern
    extName : name
    type : FuncType name
    prim : ExternPrim
    eff : Effectful

export
Eq name => Eq (Extern name) where
    MkExtern n1 t1 p1 e1 == MkExtern n2 t2 p2 e2 = p1 == p2 && e1 == e2 && n1 == n2 && t1 == t2

export
Functor Extern where
    map f (MkExtern n ty prim eff) = MkExtern (f n) (map f ty) prim eff

export
Foldable Extern where
    foldl f z (MkExtern n ty _ _) = foldl f (f z n) ty
    foldr f z (MkExtern n ty _ _) = f n $ foldr f z ty

infixl 2 <&>
(<&>) : Functor f => f (a -> b) -> a -> f b
f <&> x = ($ x) <$> f

export
Traversable Extern where
    traverse f (MkExtern n ty prim eff) = [| MkExtern (f n) (traverse f ty) |] <&> prim <&> eff

||| An entire program.
public export
record Prog name where
    constructor MkProg
    ||| External functions.
    externs : SortedMap name (Extern name)
    ||| GRIN functions.
    defs : SortedMap name (Def name)
    ||| Main function.
    mainFn : name

export
mkProg : Ord name => List (Extern name) -> List (Def name) -> (main : name) -> Prog name
mkProg exts defs m = MkProg (fromList $ pairExt <$> exts) (fromList $ pairDef <$> defs) m
  where
    pairExt : forall name. Extern name -> (name, Extern name)
    pairExt ext = (ext.extName, ext)
    pairDef : forall name. Def name -> (name, Def name)
    pairDef def = (def.defName, def)

export
Eq name => Eq (Prog name) where
    MkProg exts1 defs1 m1 == MkProg exts2 defs2 m2 = m1 == m2 && exts1 == exts2 && defs1 == defs2

export %inline
mapProg : Ord new => (old -> new) -> Prog old -> Prog new
mapProg f (MkProg exts defs m) =
    let exts' = fromList $ bimap f (map f) <$> toList exts
        defs' = fromList $ bimap f (map f) <$> toList defs
    in MkProg exts' defs' (f m)

export
Foldable Prog where
    foldl f z0 (MkProg exts defs m) =
        let z1 = foldl (foldl f) z0 exts
            z2 = foldl (foldl f) z1 defs
        in f z2 m
    foldr f z0 (MkProg exts defs m) =
        let z1 = f m z0
            z2 = foldr (flip $ foldr f) z0 exts
        in foldr (flip $ foldr f) z1 defs

export
traverseProg : Applicative t => Ord new => (old -> t new) -> Prog old -> t (Prog new)
traverseProg f (MkProg exts defs m) =
    let exts' = fromList <$> traverse (bitraverse f (traverse f)) (toList exts)
        defs' = fromList <$> traverse (bitraverse f (traverse f)) (toList defs)
    in [| MkProg exts' defs' (f m) |]

export %inline
mapExpProg : (Exp name -> Exp name) -> Prog name -> Prog name
mapExpProg f (MkProg exts defs m) = MkProg exts (map (mapExpDef f) defs) m


text:
import System
import Data.List.Views

data Palindrome : List a -> Type where
     PNil : Palindrome []
     POne : Palindrome [x]
     PRec : Palindrome xs -> Palindrome (x :: xs ++ [x])

total
palindrome : DecEq a => (xs : List a) -> Maybe (Palindrome xs)
palindrome xs with (vList xs)
  palindrome [] | VNil = Just PNil
  palindrome [x] | VOne = Just POne
  palindrome (x :: (ys ++ [y])) | (VCons z) with (decEq x y)
    palindrome (y :: (ys ++ [y])) | (VCons urec) | (Yes Refl)
       = case palindrome ys | urec of
              Nothing => Nothing
              Just x => Just (PRec x)
    palindrome (x :: (ys ++ [y])) | (VCons z) | (No contra)
       = Nothing

palinBool : DecEq a => List a -> Bool
palinBool xs = case palindrome xs of
                    Nothing => False
                    Just _ => True

main : IO ()
main = do getArgs >>= printLn
          [_, num] <- getArgs
          let list = replicate (cast num) 'a'
          printLn (palinBool list)

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Main

data Expr = Var String
          | Val Int
          | Add Expr Expr

data Eval : Type -> Type where
   MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
    fetchVal : List (String, Int) -> Maybe Int
    fetchVal [] = Nothing
    fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

implementation Functor Eval where
    map f (MkEval g) = MkEval (\e => map f (g e))

implementation Applicative Eval where
    pure x = MkEval (\e => Just x)

    (<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
       appAux : Maybe (a -> b) -> Maybe a -> Maybe b
       appAux (Just fx) (Just gx) = Just (fx gx)
       appAux _         _         = Nothing

eval : Expr -> Eval Int
eval (Var x)   = fetch x
eval (Val x)   = [| x |]
eval (Add x y) = [| eval x + eval y |]

runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e with (eval e) {
    | MkEval envFn = envFn env
}

main : IO ()
main = do printLn [| (\x => x *2) (Just 4) |]
          printLn [| plus (Just 4) (Just 5) |]
          printLn (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
          printLn (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))


text:
module Toolkit.Data.DList.Elem

import Toolkit.Data.DList

import public Toolkit.Decidable.Equality.Indexed

%default total

||| Proof that some element is found in a `DList`.
|||
||| @iTy     The type of the element's index.
||| @elemTy  The type of the list element.
||| @x       An element in the list.
||| @xs      The list itself.
||| @prf     Proof that the element's index is in the list in the same position as the element itself.
public export
data Elem : (iTy    : Type)
         -> (elemTy : iTy -> Type)
         -> forall i, is
          . (x      : elemTy i)
         -> (xs     : DList iTy elemTy is)
         -> Type
    where
      ||| Proof that the element is at the front of the list.
      H : (Equals ity elemTy x y) -> Elem ity elemTy x (y :: xs)

      ||| Proof that the element is found later in the list.
      T : (later : Elem iTy elemTy x       xs)
                -> Elem iTy elemTy x (x' ::xs)

listEmpty : Elem type e thing Nil -> Void
listEmpty (H x) impossible
listEmpty (T later) impossible

notInLater : (contraE : Equals type e x y -> Void)
          -> (contraR : Elem type e x xs -> Void)
          -> (prf    : Elem type e x (y::xs))
                    -> Void
notInLater contraE contraR (H z) = contraE z
notInLater contraE contraR (T later) = contraR later

export
isElem : {type : Type}
      -> {e    : type -> Type}
      -> DecEq type
      => DecEqIdx type e
      => {a      : type}
      -> {as     : List type}
      -> (thing  : e a)
      -> (things : DList type e as)
                -> Dec (Elem type e thing things)
isElem thing [] = No listEmpty
isElem thing (elem :: rest) with (Index.decEq thing elem)
  isElem thing (thing :: rest) | (Yes (Same Refl Refl)) = Yes (H (Same Refl Refl))
  isElem thing (elem :: rest) | (No contra) with (isElem thing rest)
    isElem thing (elem :: rest) | (No contra) | (Yes prf) = Yes (T prf)
    isElem thing (elem :: rest) | (No contra) | (No f) = No (notInLater contra f)
-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Parser

import Language.TOML.ConcreteSyntax
import Language.TOML.Tokens

import Text.Parser
import Text.Token

import Data.Bool
import Data.List
import Data.List1

-- this code does need to be repeated
-- each clause has differentl laziness
private
fromEither : {c : _} -> Grammar state token c (Either String a) -> Grammar state token c a
fromEither {c = False} act = do
    xb <- bounds act
    the (Grammar _ _ False a) $
        case xb.val of
            Right x => pure x
            Left err => failLoc xb.bounds err
fromEither {c = True} act = do
    xb <- bounds act
    the (Grammar _ _ False a) $
        case xb.val of
            Right x => pure x
            Left err => failLoc xb.bounds err

private
punct : Punctuation -> Grammar state TOMLToken True ()
punct p = match $ TTPunct p

private
maybeNewlines : Grammar state TOMLToken False ()
maybeNewlines = do
    _ <- many (punct NewLine)
    pure ()

private
newlines : Grammar state TOMLToken False ()
newlines = (some (punct NewLine) >>= \_ => pure ()) <|> eof

private
allowNewlines : (p : Grammar state TOMLToken True a) -> Grammar state TOMLToken True a
allowNewlines p = maybeNewlines *> p <* maybeNewlines

private
string : Grammar state TOMLToken True CValue
string = CVString <$> fromEither (terminal "string" getString)

private
boolean : Grammar state TOMLToken True CValue
boolean = map CVBoolean $ match TTBoolean

private
integer : Grammar state TOMLToken True CValue
integer = map CVInteger $ match TTInt

private
float : Grammar state TOMLToken True CValue
float = map CVFloat $ match TTFloat

private
bare : Grammar state TOMLToken True String
bare = match TTBare

private
key : Grammar state TOMLToken True CKey
key = do
        first <- keyAtom
        rest <- many (punct Dot *> keyAtom)
        case rest of
            [] => pure $ CKAtom first
            rest => pure $ CKDotted (first:::rest)
    where
        keyAtom : Grammar state TOMLToken True CKeyAtom
        keyAtom = map CKBare bare
              <|> (map CKQuoted $ fromEither $ terminal "string key" getKeyString)

mutual
    private
    value : Grammar state TOMLToken True CValue
    value = string
        <|> boolean
        <|> integer
        <|> float
        <|> array
        <|> inlineTable

    private
    array : Grammar state TOMLToken True CValue
    array = do
        punct (Square Open)
        commit
        vals <- sepBy (allowNewlines $ punct Comma) (allowNewlines value)
        punct (Square Close)
        pure $ CVArray vals

    private
    inlineTable : Grammar state TOMLToken True CValue
    inlineTable = do
        punct (Curly Open)
        commit
        vals <- sepBy (punct Comma) $ do
            k <- key
            punct Equal
            v <- value
            pure (k, v)

        punct (Curly Close)
        pure $ CVInlineTable vals

private
keyValue : Grammar state TOMLToken True Item
keyValue = do
    k <- key
    punct Equal
    v <- value
    newlines
    pure $ IKeyValue k v

private
tableHeader : Grammar state TOMLToken True Item
tableHeader = do
    punct (Square Open)
    k <- key
    commit
    punct (Square Close)
    newlines
    pure $ ITableHeader k

private
tableArrayHeader : Grammar state TOMLToken True Item
tableArrayHeader = do
    punct (Square Open)
    punct (Square Open)
    commit
    k <- key
    punct (Square Close)
    punct (Square Close)
    newlines
    pure $ ITableArray k

private
item : Grammar state TOMLToken True Item
item = keyValue
   <|> tableHeader
   <|> tableArrayHeader

private
items : Grammar state TOMLToken False (List Item)
items = do
    maybeNewlines
    is <- many item
    maybeNewlines
    eof
    pure is

export
parseItems : List (WithBounds TOMLToken) -> Either (List String) (List Item)
parseItems toks = case parse items $ filter (not . ignored) toks of
    Right (its, []) => Right its
    Right _ => Left ["unconsumed input"]
    Left errs => Left . flip map (forget errs) $ \(Error msg bounds) =>
        case bounds of
            Just bounds =>
                "\{show bounds.startLine}:\{show bounds.startCol}--\{show bounds.endLine}:\{show bounds.endCol}: \{msg}"
            Nothing => msg

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module Module

import Monoid
import Group
import Ring
import Group_property
import NatUtils

--(modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) ->
-- ((*) : ring -> ring -> ring) -> (IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
--This just the data required for a module, the set modu and a ring. So, this big chunk of code will appear everywhere

|||Type of operation between a ring and a moduule that distributes over addition of the ring
total
dotDistributesOverRing : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring)
                          -> ((*) : ring -> ring -> ring) -> (IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu) -> Type
dotDistributesOverRing modu ring (+) (++) (*) prfRing (.) = (r : ring) -> (s : ring) -> (m : modu) -> ((r ++ s) . m = (r . m) + (s . m))

|||Type of operation between a ring and a moduuule that distributes over addition of the Module
total
dotDistributesOverModule : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring)
                            -> ((*) : ring -> ring -> ring) -> (IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu) -> Type
dotDistributesOverModule modu ring (+) (++) (*) prfRing (.) = (m : modu) -> (n : modu) -> (r : ring) -> (r . (m + n) = (r . m) + (r . n))

|||Type of operation that respects ring multiplication
total
dotRespectsRingMult : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                       -> (IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu) -> Type
dotRespectsRingMult modu ring (+) (++) (*) prfRing (.) = (r : ring) -> (s : ring) -> (m : modu) -> ((r*s) . m = r . (s . m))

|||Type of operation that maps 1.m to m.
total
dotRespectsIdentity : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                        -> (IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu) -> Type
dotRespectsIdentity modu ring (+) (++) (*) prfRing (.) = (m : modu) -> (e . m = m) where
                                                                              e = fst (snd (fst (snd prfRing)))
|||The type of a Module. As the operations on the set modu determines it's abelianess property, we should only include the operation on the set modu and the operation between the set modu and the ring
total
IsleftModule : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                -> (IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu) -> Type
IsleftModule modu ring (+) (++) (*) prfRing (.) = ((IsAbelianGrp modu (+)) , (dotRespectsIdentity modu ring (+) (++) (*) prfRing (.) , (dotDistributesOverRing modu ring (+) (++) (*) prfRing (.) , ( dotDistributesOverModule modu ring (+) (++) (*) prfRing (.) , dotRespectsRingMult modu ring (+) (++) (*) prfRing (.)))))

--Below are a bunch of auxiliary functions to get recover dot distributing over blah from the envelope Type IsleftModule

|||Gives the Abelian Group property of a module
total
AbelianAddition : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                    -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                    -> (IsleftModule modu ring (+) (++) (*) prfRing (.)) -> (IsAbelianGrp modu (+))
AbelianAddition modu ring (+) (++) (*) prfRing (.) prfLeftModule = fst (prfLeftModule)

|||Gives the Zero of the Module
total
ZeroOfModule : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                 -> (IsleftModule modu ring (+) (++) (*) prfRing (.)) -> (e : modu ** ((a : modu) -> (a + e = a , e + a = a)))
ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule = fst (snd (fst (fst (prfLeftModule))))

|||Gives the dot distributes over Ring addition property of the module
total
dotOverRingAdd : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                  -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                   -> (IsleftModule modu ring (+) (++) (*) prfRing (.)) -> dotDistributesOverRing modu ring (+) (++) (*) prfRing (.)
dotOverRingAdd modu ring (+) (++) (*) prfRing (.) prfLeftModule = fst (snd (snd (prfLeftModule)))

|||Gives the dot distributes over module addition property of the module
total
dotOverModuleAdd : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                    -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                     -> (IsleftModule modu ring (+) (++) (*) prfRing (.)) -> dotDistributesOverModule modu ring (+) (++) (*) prfRing (.)
dotOverModuleAdd modu ring (+) (++) (*) prfRing (.) prfLeftModule = fst (snd (snd (snd (prfLeftModule))))

|||Gives the dot Associates with ring multiplication property of the module
total
dotAssociatesRingMult : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                        -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                         -> (IsleftModule modu ring (+) (++) (*) prfRing (.)) -> dotRespectsRingMult modu ring (+) (++) (*) prfRing (.)
dotAssociatesRingMult modu ring (+) (++) (*) prfRing (.) prfLeftModule = snd (snd (snd (snd (prfLeftModule))))

|||Gives the dot Associates with ring multiplication property of the module
total
dotRingIdentity : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                    -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                     -> (IsleftModule modu ring (+) (++) (*) prfRing (.)) -> dotRespectsIdentity modu ring (+) (++) (*) prfRing (.)
dotRingIdentity modu ring (+) (++) (*) prfRing (.) prfLeftModule = fst (snd (prfLeftModule))

|||Proof that r*0 = 0 for all r in the underlying ring
total
RingMultZeroEqualsZero : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                          -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                           -> (prfLeftModule : IsleftModule modu ring (+) (++) (*) prfRing (.))
                            -> ((r : ring) -> (r . (fst (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)) = (fst (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule))))
RingMultZeroEqualsZero modu ring (+) (++) (*) prfRing (.) prfLeftModule = k where
                                                                              e : modu
                                                                              e = fst (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)
                                                                              u : ring -> modu -> modu
                                                                              u r m = r . m
                                                                              f : (r : ring) -> (r . (e + e) = (r . e) + (r . e))
                                                                              f r = (dotOverModuleAdd modu ring (+) (++) (*) prfRing (.) prfLeftModule e e r)
                                                                              g : (r : ring) -> (r . (e + e) = r . e)
                                                                              g r = (cong (fst ((snd (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)) e)))
                                                                              h : (r : ring) -> (r . e = (r . e) + (r . e))
                                                                              h r = (trans (sym (g r)) (f r))
                                                                              i : (r : ring) -> ((r . e) + e = (r . e))
                                                                              i r = (fst ((snd (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)) (r . e)))
                                                                              j : (r : ring) -> ((r . e) + e = (r . e) + (r . e))
                                                                              j r = (trans (i r) (h r))
                                                                              k : (r : ring) -> ((r . e) = e)
                                                                              k r = (sym (Group_property_4 modu (+) (fst (fst prfLeftModule)) (r . e) e (r . e) (j r)))

|||Proof that 0*m = 0 for m in the module
total
ZeroMultModuleEqualsZero : (modu : Type) -> (ring : Type) -> ((+) : modu -> modu -> modu) -> ((++) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring)
                            -> (prfRing : IsRing_with_identity ring (++) (*)) -> ((.) : ring -> modu -> modu)
                             -> (prfLeftModule : IsleftModule modu ring (+) (++) (*) prfRing (.))
                              -> ((m : modu) -> ((fst (fst (snd (fst (fst prfRing))))) . m = fst (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)))
ZeroMultModuleEqualsZero modu ring (+) (++) (*) prfRing (.) prfLeftModule = k where
                                                                                e : modu
                                                                                e = fst (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)
                                                                                z : ring
                                                                                z = fst (fst (snd (fst (fst prfRing))))
                                                                                u : modu -> ring -> modu
                                                                                u m r = r . m
                                                                                f : (m : modu) -> ((z ++ z) . m = (z . m) + (z . m))
                                                                                f m = (dotOverRingAdd modu ring (+) (++) (*) prfRing (.) prfLeftModule z z m)
                                                                                g : (m : modu) -> ((z ++ z) . m = z . m)
                                                                                g m = (functionExtendsEquality2 ring modu (u m) (z ++ z) z (fst (snd (fst (snd (fst (fst prfRing)))) z)))
                                                                                h : (m : modu) -> (z . m = (z . m) + (z . m))
                                                                                h m = (trans (sym (g m)) (f m))
                                                                                i : (m : modu) -> ((z . m) + e = (z . m))
                                                                                i m = (fst ((snd (ZeroOfModule modu ring (+) (++) (*) prfRing (.) prfLeftModule)) (z . m)))
                                                                                j : (m : modu) -> ((z . m) + e = (z . m) + (z . m))
                                                                                j m = (trans (i m) (h m))
                                                                                k : (m : modu) -> ((z . m) = e)
                                                                                k m = (sym (Group_property_4 modu (+) (fst (fst prfLeftModule)) (z . m) e (z . m) (j m)))


text:
data Maybe a = Nothing
             | Just a

infixl 1 >>=

(>>=) : Maybe a -> (a -> Maybe b) -> Maybe b
(>>=) Nothing k = Nothing
(>>=) (Just x) k = k x

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

plus : Nat -> Nat -> Nat
plus Z     y = y
plus (S k) y = S (plus k y)

maybeAdd' : Maybe Nat -> Maybe Nat -> Maybe Nat
maybeAdd' x y
    = x >>= \x' =>
      y >>= \y' =>
      Just (plus x' y')

maybeAdd : Maybe Nat -> Maybe Nat -> Maybe Nat
maybeAdd x y
    = do x' <- x
         y' <- y
         Just (plus x' y')

data Either : Type -> Type -> Type where
     Left : a -> Either a b
     Right : b -> Either a b

mEmbed : Maybe a -> Maybe (Either String a)
mEmbed Nothing = Just (Left "FAIL")
mEmbed (Just x) = Just (Right x)

mPatBind : Maybe Nat -> Maybe Nat -> Maybe Nat
mPatBind x y
    = do Right res <- mEmbed (maybeAdd x y)
            | Left err => Just Z
         Just res

mLetBind : Maybe Nat -> Maybe Nat -> Maybe Nat
mLetBind x y
    = do let Just res = maybeAdd x y
                  | Nothing => Just Z
         Just res


text:
module Inigo.Async.SubtleCrypto.SubtleCrypto

import Inigo.Async.Base
import Inigo.Async.Promise
import Inigo.Async.Util

public export
data Usage : Type where
  Sign : Usage
  Verify : Usage
  (<&>) : Usage -> Usage -> Usage

infixr 5 <&>

usageArray : Usage -> List String
usageArray Sign = ["sign"]
usageArray Verify = ["verify"]
usageArray (u0 <&> u1) = (usageArray u0) ++ (usageArray u1)

interface Encodable a where
  toAnyPtr : a -> AnyPtr

public export
data EllipticCurve : Type where
  P256 : EllipticCurve
  P384 : EllipticCurve
  P512 : EllipticCurve

encodeCurve : EllipticCurve -> String
encodeCurve P256 = "P-256"
encodeCurve P384 = "P-384"
encodeCurve P512 = "P-512"

public export
data KeyAlgorithm : Type where
  KeyECDSA : EllipticCurve -> KeyAlgorithm
  KeyECDH : EllipticCurve -> KeyAlgorithm

public export
data SHA : Type where
  Sha256 : SHA
  Sha384 : SHA
  Sha512 : SHA

public export
Eq SHA where
  Sha256 == Sha256 = True
  Sha384 == Sha384 = True
  Sha512 == Sha512 = True
  _ == _ = False

export
encodeSha : SHA -> String
encodeSha Sha256 = "SHA-256"
encodeSha Sha384 = "SHA-384"
encodeSha Sha512 = "SHA-512"

export
decodeSha : String -> Maybe SHA
decodeSha "SHA-256" = Just Sha256
decodeSha "SHA-384" = Just Sha384
decodeSha "SHA-512" = Just Sha512
decodeSha _ = Nothing

public export
data Algorithm : Type where
  ECDSA : SHA -> Algorithm
  PBKDF2 : SHA -> String -> Int -> Algorithm

public export
Eq Algorithm where
  (ECDSA sha0) == (ECDSA sha1) = sha0 == sha1
  (PBKDF2 sha0 salt0 iterations0) == (PBKDF2 sha1 salt1 iterations1) = sha0 == sha1 && salt0 == salt1 && iterations0 == iterations1
  _ == _ = False

Key : Type
Key = AnyPtr
-- data Key : Type where
--   Key : AnyPtr -> Key

-- Encodable Key where
--   toAnyPtr (Key ptr) = ptr

data EncAlgo : Type where
  MkEncAlgo : AnyPtr -> EncAlgo

Encodable EncAlgo where
  toAnyPtr (MkEncAlgo ptr) = ptr

data EncKeyAlgo : Type where
  MkEncKeyAlgo : AnyPtr -> EncKeyAlgo

Encodable EncKeyAlgo where
  toAnyPtr (MkEncKeyAlgo ptr) = ptr

Signature : Type
Signature = String

inspect : String -> String
inspect str = "(function(){let inspect=(r,msg)=>{console.log(msg, r); return r;};return " ++ str ++ "})()"

arrayBufferEnc64 : String -> String
arrayBufferEnc64 str = "(function(){let arrayBufferEnc64=(buf)=>{let string = ''; (new Uint8Array(buf)).forEach((byte) => { string += String.fromCharCode(byte) }); return btoa(string);};return " ++ str ++ "})()"

arrayBufferDec64 : String -> String
arrayBufferDec64 str = "(function(){let arrayBufferDec64=(string)=>{string = atob(string); const length = string.length, buf = new ArrayBuffer(length), bufView = new Uint8Array(buf); for (var i = 0; i < length; i++) { bufView[i] = string.charCodeAt(i) } return buf;};return " ++ str ++ "})()"

%foreign "node:lambda:" ++ (arrayBufferDec64 "(name, hash, salt, iterations) => ({name, hash, salt: salt ? arrayBufferDec64(salt) : null, iterations: iterations ? iterations : null})")
encodeAlgorithm__prim : String -> String -> String -> Int -> PrimIO AnyPtr

%foreign "node:lambda:(name, namedCurve) => ({name, namedCurve})"
encodeKeyAlgorithm__prim : String -> String -> PrimIO AnyPtr

%foreign (promisifyPrim (toArray "(algo, usage, encKey) => crypto.subtle.importKey(\"jwk\", JSON.parse(encKey), algo, false, toArray(usage))"))
importKey__prim : AnyPtr -> List String -> String -> promise Key

%foreign (promisifyPrim "(key) => crypto.subtle.exportKey(\"jwk\", key).then((e) => JSON.stringify(e))")
exportKey__prim : Key -> promise String

%foreign (promisifyPrim (toArray "(algo, usage) => crypto.subtle.generateKey(algo, true, toArray(usage)).then((k) => [k.publicKey, k.privateKey]).then(__prim_js2idris_array)"))
generateKey__prim : AnyPtr -> List String -> promise (List AnyPtr)

%foreign (promisifyPrim (arrayBufferEnc64 "(algo, key, data) => crypto.subtle.sign(algo, key, new TextEncoder().encode(data)).then(arrayBufferEnc64)"))
sign__prim : AnyPtr -> AnyPtr -> String -> promise String

%foreign (promisifyPrim (arrayBufferDec64 "(algo, key, signature, data) => crypto.subtle.verify(algo, key, arrayBufferDec64(signature), new TextEncoder().encode(data)).then((res) => res ? 1 : 0)"))
verify__prim : AnyPtr -> AnyPtr -> String -> String -> promise Int

%foreign ("node:lambda:" ++ (arrayBufferEnc64 "(len) => arrayBufferEnc64(crypto.getRandomValues(new Uint8Array(len)))"))
getRand__prim : Int -> PrimIO String

%foreign (promisifyPrim (inspect (arrayBufferEnc64 "(algo, password) => crypto.subtle.importKey('raw', new TextEncoder().encode(password), algo, false, ['deriveBits', 'deriveKey']).then((km) => crypto.subtle.deriveKey(algo, km, {name:'AES-CBC','length':256}, true, ['encrypt', 'decrypt']).then((k) => crypto.subtle.exportKey('raw', k).then(arrayBufferEnc64)))")))
hash__prim : AnyPtr -> String -> promise String

encodeAlgorithm : Algorithm -> Promise EncAlgo
encodeAlgorithm (ECDSA sha) =
  map MkEncAlgo $ liftIO $ primIO (encodeAlgorithm__prim "ECDSA" (encodeSha sha) "" 0)

encodeAlgorithm (PBKDF2 sha salt iterations) =
  map MkEncAlgo $ liftIO $ primIO (encodeAlgorithm__prim "PBKDF2" (encodeSha sha) salt iterations)

encodeKeyAlgorithm : KeyAlgorithm -> Promise EncKeyAlgo
encodeKeyAlgorithm (KeyECDSA curve) =
  map MkEncKeyAlgo $ liftIO $ primIO (encodeKeyAlgorithm__prim "ECDSA" (encodeCurve curve))

encodeKeyAlgorithm (KeyECDH curve) =
  map MkEncKeyAlgo $ liftIO $ primIO (encodeKeyAlgorithm__prim "ECDH" (encodeCurve curve))

export
generateKey : KeyAlgorithm -> Usage -> Promise (Key, Key)
generateKey algo usage =
  do
    algoEnc <- encodeKeyAlgorithm algo
    (pub :: priv :: []) <- promisify (generateKey__prim (toAnyPtr algoEnc) (usageArray usage))
      | _ => reject "Invalid key generated"
    pure (pub, priv)

export
exportKey : Key -> Promise String
exportKey key =
  promisify (exportKey__prim key)

export
importKey : KeyAlgorithm -> Usage -> String -> Promise Key
importKey algo usage encKey =
  do
    algoEnc <- encodeKeyAlgorithm algo
    promisify (importKey__prim (toAnyPtr algoEnc) (usageArray usage) encKey)

export
sign : Algorithm -> Key -> String -> Promise String
sign algo key target =
  do
    algoEnc <- encodeAlgorithm algo
    promisify (sign__prim (toAnyPtr algoEnc) key target)

export
verify : Algorithm -> Key -> String -> String -> Promise Bool
verify algo key sig target =
  do
    algoEnc <- encodeAlgorithm algo
    intToBool <$> promisify (verify__prim (toAnyPtr algoEnc) key sig target)

export
getRand : Int -> Promise String
getRand len =
  do
    liftIO (primIO (getRand__prim len))

export
hash : Algorithm -> String -> Promise String
hash algo password =
  do
    algoEnc <- encodeAlgorithm algo
    promisify (hash__prim (toAnyPtr algoEnc) password)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Instances.Notation

import public Data.Vect
import public Data.Rel
import public Decidable.Decidable
import Common.Abbrev
import Common.Interfaces
import Specifications.DiscreteOrderedGroup
import Specifications.OrderedRing

%default total
%access public export

specifyMonoid : Ringops s => Type
specifyMonoid {s} = MonoidSpec {s} (+) Zero

specifyGroup : Ringops s => Type
specifyGroup {s} = GroupSpec {s} (+) Zero Ng

specifyPartialOrder : Decidable [s,s] leq => Type
specifyPartialOrder {leq} = PartialOrderSpec leq

specifyTotalOrder : Decidable [s,s] leq => Type
specifyTotalOrder {leq} = TotalOrderSpec leq

specifyPartiallyOrderedMagma : (Ringops s, Decidable [s,s] leq) => Type
specifyPartiallyOrderedMagma {leq} = PartiallyOrderedMagmaSpec (+) leq

specifyPartiallyOrderedGroup : (Ringops s, Decidable [s,s] leq) => Type
specifyPartiallyOrderedGroup {leq} = PartiallyOrderedGroupSpec (+) Zero Ng leq

specifyOrderedGroup : (Ringops s, Decidable [s,s] leq) => Type
specifyOrderedGroup {leq} = OrderedGroupSpec (+) Zero Ng leq

specifyDiscreteOrderedGroup : (Ringops s, Decidable [s,s] leq) => Type
specifyDiscreteOrderedGroup {leq} =
  DiscreteOrderedGroupSpec (+) Zero Ng leq One

specifyRing : Ringops s => Type
specifyRing {s} = RingSpec {s} (+) Zero Ng (*)

specifyPartiallyOrderedRing : (Ringops s, Decidable [s,s] leq) => Type
specifyPartiallyOrderedRing {leq} =
  PartiallyOrderedRingSpec (+) Zero Ng (*) leq

specifyOrderedRing : (Ringops s, Decidable [s,s] leq) => Type
specifyOrderedRing {leq} =
  OrderedRingSpec (+) Zero Ng (*) leq

specifyDiscreteOrderedRing : (Ringops s, Decidable [s,s] leq) => Type
specifyDiscreteOrderedRing {leq} =
  DiscreteOrderedRingSpec (+) Zero Ng (*) leq One

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Bautzen.REPL

import Debug.Trace
import Bautzen.Game
import Bautzen.Options
import Bautzen.REPL.SExpParser
import Bautzen.REPL.SExpInstances
import Bautzen.SExp

import System.REPL.Extra

import Data.Fin
import Data.Nat

data CmdREPL : (segment : GameSegment) -> Type where
  Cmd : (cmd : Command segment) -> CmdREPL segment
  Qry : (ToSExp res) => (qry : Query res) -> CmdREPL segment

makePos : (col : Int) -> (row : Int) -> Either String Pos
makePos col row with (integerToNat (cast col), integerToNat (cast row))
  makePos col row | (c , r) with (isLTE c 22, isLTE r 12)
  makePos col row | (c , r)  | (Yes _, Yes _) = Right $ Hex c r
  makePos col row | (c , r)  | _              = Left $ "position should be between (0,0) and (22, 12): " ++ show col ++ ", " ++ show row

makeMoveCommand : (unitName : String) -> (col : Int) -> (row : Int) -> Either String (Command Move)
makeMoveCommand unitName col row = MoveTo unitName <$> makePos col row

makeAttackWithCommand : (unitNames : SExp) -> (col : Int) -> (row : Int) -> Either String (Command $ Combat NoCombat)
makeAttackWithCommand unitNames col row = do
  pos <- makePos col row
  units <- toStrings unitNames
  pure $ AttackWith units pos

makeSupportCommand : (unitNames : SExp) -> {side : Side} -> {combatState : CombatState}
                   -> Either String (Command $ Combat (AssignTacticalSupport side combatState))
makeSupportCommand unitNames =
  toStrings unitNames >>= Right . TacticalSupport

makeLoseStepCommand : (unitName : String) -> {side : Side} -> {combatState : CombatState}
                   -> Either String (Command $ Combat (ApplyLosses side combatState))
makeLoseStepCommand unitName = pure $ LoseStep unitName

foo : (game : Game) -> String -> String
foo game s with (curSegment game)
  foo game s | Move = "Move"
  foo game s | _ = "other"

makeCommand : (game : Game) -> SExp -> Either String (CmdREPL (curSegment game))
makeCommand game (SList [ SSym "move!", SStr unitName, SList [ SInt col, SInt row] ] ) with (curSegment game)
  makeCommand game (SList [ SSym "move!", SStr unitName, SList [ SInt col, SInt row] ] ) | Move = Cmd <$> makeMoveCommand unitName col row
  makeCommand game (SList [ SSym "move!", SStr unitName, SList [ SInt col, SInt row] ] ) | other = Left ("Invalid command for segment " ++ show other)
makeCommand game (SList [ SSym "attack!", unitNames, SList [ SInt col, SInt row] ] ) with (curSegment game)
  makeCommand game (SList [ SSym "attack!", unitNames, SList [ SInt col, SInt row] ] ) | Combat NoCombat = Cmd <$> makeAttackWithCommand unitNames col row
  makeCommand game (SList [ SSym "attack!", unitNames, SList [ SInt col, SInt row] ] ) | other = Left $ "Invalid command for segment " ++ show other
makeCommand game (SList [ SSym "support!", unitNames ] ) with (curSegment game)
  makeCommand game (SList [ SSym "support!", unitNames ] ) | Combat (AssignTacticalSupport side combatState) = Cmd <$> makeSupportCommand unitNames
  makeCommand game (SList [ SSym "support!", unitNames ] ) | other = Left $ "Invalid command for segment " ++ show other
makeCommand game (SList [ SSym "resolve!" ] ) with (curSegment game)
  makeCommand game (SList [ SSym "resolve!" ] ) | Combat (Resolve combatState) = pure $ Cmd (ResolveCombat combatState)
  makeCommand game (SList [ SSym "resolve!" ] ) | other = Left $ "Invalid command for segment " ++ show other
makeCommand game (SList [ SSym "lose-step!", SStr unitName ] ) with (curSegment game)
  makeCommand game (SList [ SSym "lose-step!", SStr unitName ] ) | Combat (ApplyLosses side state) = Cmd <$> makeLoseStepCommand unitName
  makeCommand game (SList [ SSym "lose-step!", SStr unitName ] ) | other = Left $ "Invalid command for segment " ++ show other
makeCommand game (SList [ SSym "next!" ] ) = pure $ Cmd NextSegment
makeCommand game (SList [ SSym "supply-path?", SStr unitName ] ) = Right $ Qry $ SupplyPath unitName
makeCommand game (SList [ SSym "map?" ] ) = Right $ Qry TerrainMap
makeCommand game (SList [ SSym "positions?" ] ) = Right $ Qry Positions
makeCommand game (SList [ SSym "stage?" ] ) = Right $ Qry GameStage
makeCommand _ sexp = Left $ "Unknown command " ++ show sexp

partial
parseCommand : (game : Game) -> String -> Either String (CmdREPL (curSegment game))
parseCommand game input = do
  sexp <- parseSExp input
  makeCommand game sexp

partial
export
commandHandler : Game -> String -> (String, Game)
commandHandler game command =
  case parseCommand game command of
    Left err => (err, game)
    Right (Cmd cmd) => case act game cmd of
                         Left err => (show (toSExp err), game)
                         Right event => (show (toSExp event), apply event game)
    Right (Qry qry) =>
      let qryResult = toSExp $ query game qry
      in (show qryResult, game)

partial
eoiHandler : Game -> String
eoiHandler = show

initialPositions : List (GameUnit, Pos)
initialPositions = [ (Bautzen.GameUnit.p13_5dp, Hex 1 9)
                   , (Bautzen.GameUnit.g21_20pz, Hex 5 8)
                   ]

initialState : GameState
initialState = MkGameState 5 Axis Move initialPositions

export
initialGame : Game
initialGame = MkGame [] initialState FullGameMap

export
partial
repl : Options -> IO ()
repl _ = processStdin initialGame commandHandler eoiHandler

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


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

%name Vect xs, ys, zs

curry : ((a, b) -> c) -> a -> b -> c
curry f x y = ?curry_rhs

uncurry : (a -> b -> c) -> (a, b) -> c
uncurry f x = ?uncurry_rhs

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ?append_rhs_1
append (x :: xs) ys = ?append_rhs_2

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f [] [] = ?zipWith_rhs_1
zipWith f (x :: xs) (y :: ys) = ?zipWith_rhs_2


text:
module Utils.String

%default total

export
dotSep : List String -> String
dotSep [] = ""
dotSep [x] = x
dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]

export
stripQuotes : (str : String) -> String
stripQuotes str = substr 1 (length str `minus` 2) str


text:
module Main

import IdrisScript
import IdrisScript.Timer

main : JS_IO ()
main = do
  setInterval (\_ => print "PING!") 1000
  putStrLn "Done!"

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Matrix

import Data.Vect
import fn_to_vect

%access public export

ZeroRow : (n : Nat) -> (typ : Type) -> (zero : typ) -> Vect n typ
ZeroRow Z typ zero = []
ZeroRow (S n) typ zero = zero::(ZeroRow n typ zero)

total
ZeroMat : (n : Nat) -> (m : Nat) -> (typ : Type) -> (zero : typ) -> Vect n (Vect m typ)
ZeroMat Z m typ zero = []
ZeroMat (S n) m typ zero = (ZeroRow m typ zero) :: (ZeroMat n m typ zero)

total
innerPdt : (n : Nat) -> (typ : Type) -> ((*) : typ -> typ -> typ) ->
           ((+) : typ -> typ -> typ) -> (zero : typ) ->
           Vect n typ -> Vect n typ -> typ

innerPdt Z typ (*) (+) zero [] [] = zero
innerPdt (S k) typ (*) (+) zero (x::xs) (y::ys) =
    x*y + (innerPdt k typ (*) (+) zero xs ys)

total
mulVect : (m : Nat) -> (k : Nat) -> (typ : Type) ->
          ((*) : typ -> typ -> typ) ->
          ((+) : typ -> typ -> typ) -> (zero : typ) ->
          Vect m typ -> Vect m (Vect k typ) -> Vect k typ

mulVect m k typ (*) (+) zero x ys = map (innerPdt m typ (*) (+) zero x) (transpose ys)

mulMat : (n : Nat) -> (m : Nat) -> (k : Nat) -> (typ : Type) ->
         ((*) : typ -> typ -> typ) -> ((+) : typ -> typ -> typ) -> (zero : typ) ->
         Vect n (Vect m typ) -> Vect m (Vect k typ) -> Vect n (Vect k typ)

mulMat Z m k typ (*) (+) zero [] xs = []
mulMat (S n) m k typ (*) (+) zero (x::xs) ys =
    (mulVect m k typ (*) (+) zero x ys)::(mulMat n m k typ (*) (+) zero xs ys)

Identity_Bool : (n : Nat) -> (Mat_Vect n n Bool)
Identity_Bool n = Diag_Mat_Vect n Bool False True

addMat : (n : Nat) -> (m : Nat) -> (ty : Type) ->
         ((+) : ty -> ty -> ty) -> (Mat_Vect n m ty) ->
         (Mat_Vect n m ty) -> (Mat_Vect n m ty)
addMat n m ty (+) u v = (Mat_fn_to_Vect n m ty fn) where
    fn_u : Mat_fn n m ty
    fn_u = Mat_Vect_to_fn n m ty u

    fn_v : Mat_fn n m ty
    fn_v = Mat_Vect_to_fn n m ty v

    fn : Mat_fn n m ty
    fn i j = (fn_u i j) + (fn_v i j)


text:
import Data.Vect
import Data.Vect.Elem

-- removeElem : {n : _ } -> (value : a) -> (xs : Vect (S n) a) -> (prf : Elem value xs) -> Vect n a
-- removeElem value (value :: xs) Here = xs
-- removeElem {n = Z} value (y :: []) (There later) = absurd later
-- removeElem {n = (S k)} value (y :: xs) (There later) = y :: removeElem value xs later

-- removeElem_auto : {n : _} -> (value : a) ->
--                   (xs : Vect (S n) a) ->
--                   (prf : Elem value xs) =>
--                   Vect n a
-- removeElem_auto value xs = removeElem value xs prf

public export
removeElem : {n : _ } ->
             (value : a) ->
             (xs : Vect (S n) a) ->
             (prf : Elem value xs) =>
             Vect n a
removeElem value (value :: xs) {prf = Here} = xs
removeElem {n = Z} value (y :: []) {prf = (There later)} = absurd later
removeElem {n = (S k)} value (y :: xs) {prf = (There later)} = y :: removeElem value xs


text:
module QuantumOp

import Data.Vect
import Data.Nat
import Decidable.Equality
import System.File
import Injection
import Matrix
import Complex
import System.Random
import Lemmas
import QStateT
import Control.Linear.LIO
import LinearTypes
import Unitary

||| The Qubit type is used to identify individual qubits. The Nat argument is
||| used to uniquely identify a qubit. This type does *not* carry any quantum
||| state information. The constructor MkQubit is *private* in order to prevent
||| pattern matching by users of the library.
export
data Qubit : Type where
  MkQubit : (n : Nat) -> Qubit

||| The QuantumOp interface is used to abstract over the representation of a
||| quantum state. It is parameterised by the number of qubits it contains.
export
interface QuantumOp (0 t : Nat -> Type) where

  ||| Prepare 'p' new qubits in state |00...0>
  newQubits : (p : Nat) -> QStateT (t n) (t (n+p)) (LVect p Qubit)
  newQubits Z     = rewrite plusZeroRightNeutral n in pure []
  newQubits (S k) = rewrite lemmaPlusSRight n k in do
    q <- newQubit
    qs <- newQubits k
    pure (q :: qs)

  ||| Prepare a single new qubit in state |0>
  newQubit : QStateT (t n) (t (S n)) Qubit
  newQubit = rewrite sym $ lemmaplusOneRight n in do
    [q] <- newQubits 1
    pure q

  ||| Apply a unitary circuit to the qubits specified by the LVect argument
  applyUnitary : {n : Nat} -> {i : Nat} ->
                 (1 _ : LVect i Qubit) -> Unitary i -> QStateT (t n) (t n) (LVect i Qubit)

  ||| Apply the Hadamard gate to a single qubit
  applyH : {n : Nat} -> (1 _ : Qubit) -> QStateT (t n) (t n) Qubit
  applyH q = do
    [q1] <- applyUnitary {n} {i = 1} [q] HGate
    pure q1

  ||| Apply a P gate to a single qubit
  applyP : {n : Nat} -> Double -> (1 _ : Qubit) -> QStateT (t n) (t n) Qubit
  applyP p q = do
    [q1] <- applyUnitary {n} {i = 1} [q] (PGate p)
    pure q1

  ||| Apply the CNOT gate to a pair of qubits
  applyCNOT : {n : Nat} -> (1 _ : Qubit) -> (1 _ : Qubit) -> QStateT (t n) (t n) (LPair Qubit Qubit)
  applyCNOT q1 q2 = do
    [q1,q2] <- applyUnitary {n} {i = 2} [q1,q2] CNOTGate
    pure (q1 # q2)

  ||| Measure some qubits in a quantum state
  public export
  measure : {n : Nat} -> {i : Nat} -> (1 _ : LVect i Qubit) -> QStateT (t (i + n)) (t n) (Vect i Bool)
  measure [] = pure []
  measure (q :: qs) = do
    b <- measureQubit q
    bs <- measure qs
    pure (b `consLin` bs)

  ||| Measure only one qubit
  measureQubit : {n : Nat} -> (1 _ : Qubit) -> QStateT (t (S n)) (t n) Bool
  measureQubit q = do
    [b] <- measure [q]
    pure b

  ||| Same as measure, but with an initial state of n + i instead of i + n qubits to help with theorem proving in some cases
  -- public export
  -- measure2 : {n : Nat} -> {i : Nat} -> (LVect i Qubit) -> QStateT (t (n + i)) (t n) (Vect i Bool)
  -- measure2 v = rewrite plusCommutative n i in measure v

  ||| Measure all qubits in a quantum state
  ||| Because of a bug in Idris2, we use the implementation below.
  ||| However, the implementation commented out is preferable if the bug gets fixed.
  public export
  measureAll : {n : Nat} -> (1 _ : LVect n Qubit) -> QStateT (t n) (t 0) (Vect n Bool)
  measureAll []        = pure []
  measureAll (q :: qs) = do
    b <- measureQubit q
    bs <- measureAll qs
    pure (b `consLin` bs)
  --measureAll qs = rewrite sym $ plusZeroRightNeutral n in measure qs

  ||| Execute a quantum operation : start and finish with trivial quantum state
  ||| (0 qubits) and measure 'n' qubits in the process
  run : QStateT (t 0) (t 0) (Vect n Bool) -> IO (Vect n Bool)

----- IMPLEMENTATION OF QUANTUMSTATE: LINEAR-ALGEBRAIC SIMULATION -----------

||| SimulatedOp : linear-algebraic vector representation of the quantum state, vector of indices of the qubits, counter
export
data SimulatedOp : Nat -> Type where
  MkSimulatedOp : {n : Nat} -> Matrix (power 2 n) 1 -> Vect n Qubit -> Nat -> SimulatedOp n

------ SIMULATION : AUXILIARY (PRIVATE) FUNCTIONS ------

||| Find an element in a list : used to find the wire of a qubit
private
listIndex' : {n : Nat} -> Vect n Qubit -> Qubit -> Nat
listIndex' [] _ = 0
listIndex' (MkQubit x :: xs) (MkQubit k) = if x == k then 0 else S (listIndex' xs (MkQubit k))

private
listIndex : (1 _ : SimulatedOp n) -> (1 _ : Qubit) -> LFstPair (LPair (SimulatedOp n) Qubit) Nat
listIndex (MkSimulatedOp qs v counter) (MkQubit k) = (MkSimulatedOp qs v counter # MkQubit k) # (listIndex' v (MkQubit k))

private
listIndices : (1 _ : SimulatedOp n) -> (1 _ : LVect i Qubit) -> LFstPair (LPair (SimulatedOp n) (LVect i Qubit)) (Vect i Nat)
listIndices qs [] = (qs # []) # []
listIndices qs (x :: xs) =
  let (qs' # x') # y = listIndex qs x
      (qs2 # xs') # ys = listIndices qs' xs
  in (qs2 # (x' :: xs')) # (y :: ys)

||| Remove an element at a given index in the vector
private
removeElem : {n : Nat} -> Vect (S n) Qubit -> Nat -> Vect n Qubit
removeElem (x :: xs) 0 = xs
removeElem (x :: xs) (S k) = case xs of
                                  [] => []
                                  y :: ys => x :: removeElem xs k

||| add the indices of the new qubits to the vector in the SimulatedOp
private
newQubitsPointers : (p : Nat) -> (counter : Nat) -> LFstPair (LVect p Qubit) (Vect p Qubit)
newQubitsPointers 0 _ = ([] # [])
newQubitsPointers (S p) counter =
  let (q # v) = newQubitsPointers p (S counter)
  in (MkQubit counter :: q) #  (MkQubit counter :: v)

||| Auxiliary function for applying a circuit to some qubits
private
applyUnitary' : {n : Nat} -> {i : Nat} ->
                (1 _ : LVect i Qubit) -> Unitary i -> (1 _ : SimulatedOp n) -> R (LPair (SimulatedOp n) (LVect i Qubit))
applyUnitary' v u q =
  let (qs # v') # ind = listIndices q v
      qs2 = applyCirc ind u qs
  in pure1 (qs2 # v') where
    applyCirc : Vect i Nat -> Unitary i -> (1 _ : SimulatedOp n) -> SimulatedOp n
    applyCirc v IdGate qst = qst
    applyCirc v (H j g) st =
      let k = index j v
          h = simpleTensor matrixH n k
          MkSimulatedOp qst q counter = applyCirc v g st
      in MkSimulatedOp (h `matrixMult` qst) q counter
    applyCirc v (P p j g) st =
      let k = index j v
          ph = simpleTensor (matrixP p) n k
          MkSimulatedOp qst q counter = applyCirc v g st
      in MkSimulatedOp (ph `matrixMult` qst) q counter
    applyCirc v (CNOT c t g) st =
      let kc = index c v
          kt = index t v
          cn =  tensorCNOT n kc kt
          MkSimulatedOp qst q counter = applyCirc v g st
      in MkSimulatedOp (cn `matrixMult` qst) q counter

||| Auxiliary function for measurements
private
measure' : {n : Nat} -> (i : Nat) ->
           (1 _ : SimulatedOp (S n)) ->
           R (LFstPair (SimulatedOp n) Bool)
measure' {n} i (MkSimulatedOp v w counter) = do
  let projector0 = simpleTensor matrixKet0Bra0 (S n) i
  let projection0 = projector0 `matrixMult` v
  let norm20 = normState2 projection0
  let projector1 = simpleTensor matrixKet1Bra1 (S n) i
  let projection1 = projector1 `matrixMult` v
  let norm21 = normState2 projection1
  let newQubits = removeElem w i
  randnb <- liftIO1 randomIO
  if randnb < norm20
     then do
       let proj = multScalarMatrix (inv (sqrt norm20) :+ 0) projection0
       pure1 (MkSimulatedOp (projectState {n} proj i False) newQubits counter # False)
     else do
       let proj = multScalarMatrix (inv (sqrt norm21) :+ 0) projection1
       pure1 (MkSimulatedOp (projectState {n} proj i True) newQubits counter # True)

||| Auxiliary function for measurements
private
measureQubits' : {n : Nat} -> {i : Nat} ->
                 (1 _ : LVect i Qubit) ->
                 (1 _ : SimulatedOp (i + n)) -> R (LPair (SimulatedOp n) (Vect i Bool))
measureQubits' [] qs = pure1 (qs # [])
measureQubits' (x :: xs) qs = do
  let (qs' # (MkQubit k)) # y = listIndex qs x
  (s # b) <- measure' y qs'
  (s1 # bs) <- measureQubits' xs s
  case bs of
       [] => pure1 (s1 # [b])
       (b' :: bs') => pure1 (s1 # (b :: b' :: bs'))

------- SIMULATE CIRCUITS : OPERATIONS ON QUANTUM STATES ------

||| Add new qubits to a Quantum State
export
newQubitsSimulated : (p : Nat) -> QStateT (SimulatedOp n) (SimulatedOp (n+p)) (LVect p Qubit)
newQubitsSimulated p = MkQST (newQubits' p) where
  newQubits' : (q : Nat) -> (1 _ : SimulatedOp m) -> R (LPair (SimulatedOp (m + q)) (LVect q Qubit))
  newQubits' q (MkSimulatedOp qs v counter) =
    let s' = toTensorBasis (ket0 q)
        (qubits # v') = newQubitsPointers q counter
    in pure1 (MkSimulatedOp (tensorProductVect qs s') (v ++ v') (counter + q) # qubits)

||| Apply a unitary circuit to a SimulatedOp
export
applyUnitarySimulated : {n : Nat} -> {i : Nat} ->
               (1 _ : LVect i Qubit) -> Unitary i -> QStateT (SimulatedOp n) (SimulatedOp n) (LVect i Qubit)
applyUnitarySimulated q u = MkQST (applyUnitary' q u)

||| Measure some qubits in a quantum state
export
measureSimulated : {n : Nat} -> {i : Nat} -> (1 _ : LVect i Qubit) -> QStateT (SimulatedOp (i + n)) (SimulatedOp n) (Vect i Bool)
measureSimulated v = MkQST (measureQubits' v)

||| Run all simulations : start with 0 qubit and measure all qubits at the end (end with 0 qubit)
export
runSimulated : QStateT (SimulatedOp 0) (SimulatedOp 0) (Vect n Bool) -> IO (Vect n Bool)
runSimulated s = LIO.run (do
  ((MkSimulatedOp st w c) # v) <- runQStateT (MkSimulatedOp [[1]] [] 0) s
  case v of
       [] => pure []
       (x :: xs) => pure (x :: xs))

export
QuantumOp SimulatedOp where
  newQubits    = newQubitsSimulated
  applyUnitary = applyUnitarySimulated
  measure      = measureSimulated
  run          = runSimulated

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
-- Example of a union type.
||| Represents shapes.
data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its lengths and height
             Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

area : Shape -> Double
area (Triangle base height) = base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius


text:
module BTree

%default total

public export
data BTree : Type -> Type where
  Leaf : BTree a
  Node : BTree a -> a -> BTree a -> BTree a

export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x tree@(Node l v r) = case compare x v of
                              LT => Node (insert x l) v r
                              GT => Node l v (insert x r)
                              EQ => tree

export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = toList l ++ [v] ++ toList r

export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Ch05.Exercise_5_2_5

import Ch05.LambdaCalculus

%default total

||| `sub m n` yields the result of subtracting `n` from `m` (Church numerals).
|||
||| More precisely, it yields the smallest church numeral `z` such that
|||
|||     m <= n+z
public export
sub : Term
sub = let m = Var 0
          n = Var 1 in
          Abs 0 (Abs 1 (n . prd) . m)

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Hezarfen.FunDefn

import Hezarfen.Prover
import Hezarfen.Simplify
import Language.Reflection.Utils

%access public export

||| Looking at a proof term, collect the initial lambda argument names and
||| their types, and return the remaining proof term after the initial lambdas.
collect : Tm -> (List (TTName, Ty), Tm)
collect (RBind n' (Lam b) t') with (collect t')
  | (xs, rest) = ((n', b) :: xs, rest)
collect t' = ([], t')

||| Returns a left and right hand side for a fun clause
lambdas : TTName -> Tm -> Elab (Tm, Tm)
lambdas n t =
    let (xs, rhs) = collect t in
    let apps = foldl (\t, (name, _) => RApp t (Var name)) (Var n) xs in
    let xsRev = reverse xs in
    pure (binds xsRev apps, binds xsRev rhs)
  where
    ||| The list should be reversed beforehand
    binds : List (TTName, Ty) -> Tm -> Raw
    binds [] t' = t'
    binds ((n', ty) :: xs) t' = binds xs $ RBind n' (PVar ty) t'

||| Takes a list of the arguments parsed by `collect`, and the rest of
||| the proof term. Checks how many consecutive `fst` and `snd` projections
||| in the beginning of `rest`. Returns a list of the names of the pairs they
||| project on, and what the projections are named. Also returns the rest
||| of the proof term stripped from the projections.
pairProjections : (lamIntro : List (TTName, Tm)) -> (rest : Tm)
               -> Elab (List (TTName, (TTName, TTName)), Tm)
pairProjections lamIntro rest =
  case rest of
    RBind n1 (Let a `(Prelude.Basics.fst {a=~a1} {b=~b1} ~(Var p1)))
      (RBind n2 (Let b `(Prelude.Basics.snd {a=~a2} {b=~b2} ~(Var p2))) t) =>
      if p1 == p2 && (p1 `elem` (fst <$> lamIntro)) && not (p1 `isBound` t)
         then do (xs, t') <- pairProjections lamIntro t
                 pure ((p1, (n1, n2)) :: xs, t)
         else pure ([], rest)
    RBind n b t =>
      if n `elem` (fst <$> lamIntro)
         then pure ([], rest)
         else do (xs, t') <- pairProjections lamIntro t
                 pure (xs, RBind n b t')
    RApp t1 t2 =>
      do (xs, t1') <- pairProjections lamIntro t1
         (ys, t2') <- pairProjections lamIntro t2
         pure (xs ++ ys, RApp t1' t2')
    _ => pure ([], rest)

||| The entry point for other modules.
definitionize : TTName -> Tm -> Elab (FunDefn Raw)
definitionize n t =
  let (lhs, rhs) = !(lambdas n t) in
  -- TODO figure out how to create LHS and RHS that respects the pair patterns
  -- let (pairReplacements, rest) = pairProjections _ rhs
  pure $ DefineFun n [MkFunClause lhs rhs]

max_stars_repo_name: joom/hezarfen

max_issues_repo_name: joom/hezarfen

max_forks_repo_name: joom/hezarfen


text:
module Minecraft.Core.Entity.Export

import public Minecraft.Core.Entity
import public Minecraft.Core.Tangible

%default total

public export
Entity e => Tangible e where

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Test

import System

import Text.PrettyPrint.Leijen

%default total

--%access private

data SExpr = Symbol String
           | (::) SExpr SExpr
           | Nil
           | IntLit Int

consp : SExpr -> Bool
consp (_ :: _) = True
consp _ = False

mutual
  pprint : SExpr -> Doc
  pprint (Symbol str) = text str
  pprint (IntLit i)   = text (show i)
  pprint (x :: y)   = enclose lparen rparen (align $ listContents x y)
  pprint Nil          = lparen |+| rparen

  listContents : SExpr -> SExpr -> Doc
  listContents car Nil = pprint car
  listContents car (Symbol str) = pprint car |++| dot |++| pprint (Symbol str)
  listContents car (IntLit i) = pprint car |++| dot |++| pprint (IntLit i)
  listContents car (cadr :: cddr) = group $ pprint car |$| listContents cadr cddr

fromString : String -> SExpr
fromString x = Symbol x

omega : SExpr
omega = [[Symbol "lambda", [Symbol "f"], [Symbol "f", Symbol "f"]], [Symbol "lambda", [Symbol "f"], [Symbol "f", Symbol "f"]]]

covering
test : Nat -> SimpleDoc
test w = renderPretty 0.8 w (pprint omega)

covering
test1 : String
test1 = displayS (test 80) ""

covering
test2 : String
test2 = displayS (test 40) ""

covering
test3 : String
test3 = displayS (test 20) ""

covering
test4 : String
test4 = displayS (test 10) ""

doTest : String -> String -> IO ()
doTest output expected =
  if output == expected
    then putStrLn "ok"
    else do putStrLn $ "Expected: " ++ expected
            putStrLn $ "Got: " ++ output
            exitFailure

public export covering
main : IO ()
main = traverse_ (uncurry doTest)
            [ (test1, "((lambda (f) (f f)) (lambda (f) (f f)))")
            , (test2, "((lambda (f) (f f))\n (lambda (f) (f f)))")
            , (test3, "((lambda\n  (f) (f f))\n (lambda\n  (f) (f f)))")
            , (test4, "((lambda\n  (f)\n  (f f))\n (lambda\n  (f)\n  (f f)))")
            ]


text:
-- expressions

data SourcePos = SP String Nat Nat
Show SourcePos where
  show (SP x k j) = x ++ ":" ++ (show k) ++ "," ++ (show j)

one : Nat
one = unsafePerformIO $ do putStrLn "ALEX"
                           pure 3

data Name = Name' String

Show Name where
  show (Name' x) = x

Eq Name where
  (==) (Name' x) (Name' y) = x == y

data Expr
  = Var Name   -- x
  | Pi Name Expr Expr -- (Π ((x A)) B)
  | Lambda Name Expr -- (λ (x) b)
  | App Expr Expr -- (rator rand)
  | Sigma Name Expr Expr -- (Σ ((x A)) D)
  | Cons Expr Expr -- (cons a d)
  | Car Expr -- (car e)
  | Cdr Expr -- (cdr e)
  | Nat -- Nat
  | Zero -- zero
  | Add1 Expr -- (add1 e)
  | IndNat Expr Expr Expr Expr -- (ind-nat tgt mot base step)
  | Equal Expr Expr Expr -- (= A from to)
  | Same -- Same
  | Replace Expr Expr Expr -- (replace tgt mot base)
  | Trivial -- Trivial
  | Sole -- sole
  | Absurd -- Absurd
  | IndAbsurd Expr Expr -- (ind-Absurd tgt mot)
  | Atom -- Atom
  | Tick String -- 'a
  | U -- U
  | The Expr Expr -- (the t e)
  | SrcPos SourcePos Expr

Show Expr where
Eq Expr where

Namespace : Type
Namespace = List (Name, Integer)
%name Namespace ns1, ns2, ns3

-- alpha equivalence
aEquivHelper : (i : Integer) ->
               Namespace -> Expr ->
               Namespace -> Expr ->
               Bool
aEquivHelper i ns1 (Var x) ns2 (Var y) =
  case (lookup x ns1, lookup y ns2) of
       (Nothing, Nothing) => x == y
       (Just j, Just k) => i == j
       _ => False

aEquivHelper i ns1 (Pi x a1 r1) ns2 (Pi y a2 r2) =
  aEquivHelper i ns1 a1 ns2 a2 &&
  aEquivHelper (i+1) ((x, i) :: ns1) r1 ((y, i) :: ns2) r2

aEquivHelper i ns1 (Lambda x body1) ns2 (Lambda y body2) =
  aEquivHelper (i+1) ((x, i) :: ns1) body1 ((y, i) :: ns2) body2

aEquivHelper i ns1 (App rator1 rand1) ns2 (App rator2 rand2) =
  aEquivHelper i ns1 rator1 ns2 rator2 &&
  aEquivHelper i ns1 rand1 ns2 rand2

aEquivHelper i ns1 (Sigma x a1 d1) ns2 (Sigma y a2 d2) =
  aEquivHelper i ns1 a1 ns2 a2 &&
  aEquivHelper (i+1) ((x, i) :: ns1) d1 ((y, i) :: ns2) d2

aEquivHelper i ns1 (Cons car1 cdr1) ns2 (Cons car2 cdr2) =
  aEquivHelper i ns1 car1 ns2 car2 &&
  aEquivHelper i ns1 cdr1 ns2 cdr2

aEquivHelper i ns1 (Car pair1) ns2 (Car pair2) =
  aEquivHelper i ns1 pair1 ns2 pair2
aEquivHelper i ns1 (Cdr pair1) ns2 (Cdr pair2) =
  aEquivHelper i ns1 pair1 ns2 pair2

aEquivHelper _ _ Nat _ Nat = True
aEquivHelper _ _ Zero _ Zero = True

aEquivHelper i ns1 (Add1 e1) ns2 (Add1 e2) =
  aEquivHelper i ns1 e1 ns2 e2

aEquivHelper i ns1 (IndNat tgt1 mot1 base1 step1) ns2 (IndNat tgt2 mot2 base2 step2) =
  aEquivHelper i ns1 tgt1 ns2 tgt2 &&
  aEquivHelper i ns1 mot1 ns2 mot2 &&
  aEquivHelper i ns1 base1 ns2 base2 &&
  aEquivHelper i ns1 step1 ns2 step2

aEquivHelper i ns1 (Equal ty1 from1 to1) ns2 (Equal ty2 from2 to2) =
  aEquivHelper i ns1 ty1 ns2 ty2 &&
  aEquivHelper i ns1 from1 ns2 from2 &&
  aEquivHelper i ns1 to1 ns2 to2

aEquivHelper _ _ Same _ Same = True

aEquivHelper i ns1 (Replace tgt1 mot1 base1) ns2 (Replace tgt2 mot2 base2) =
  aEquivHelper i ns1 tgt1 ns2 tgt2 &&
  aEquivHelper i ns1 mot1 ns2 mot2 &&
  aEquivHelper i ns1 base1 ns2 base2

aEquivHelper _ _ Trivial _ Trivial = True
aEquivHelper _ _ Sole _ Sole = True
aEquivHelper _ _ Absurd _ Absurd = True
aEquivHelper _ _ Atom _ Atom = True
aEquivHelper _ _ U _ Atom = True

aEquivHelper i ns1 (IndAbsurd tgt1 mot1) ns2 (IndAbsurd tgt2 mot2) =
  aEquivHelper i ns1 tgt1 ns2 tgt2 &&
  aEquivHelper i ns1 mot1 ns2 mot2

aEquivHelper i ns1 (Tick a1) ns2 (Tick a2) = a1 == a2

aEquivHelper _ _ (The Absurd _) _ (The Absurd _) = True
aEquivHelper i ns1 (The t1 e1) ns2 (The t2 e2) =
  aEquivHelper i ns1 t1 ns2 t2 &&
  aEquivHelper i ns1 e1 ns2 e2

aEquivHelper i ns1 (SrcPos str1 e1) ns2 (SrcPos str2 e2) =
  aEquivHelper i ns1 e1 ns2 e2

aEquivHelper _ _ _ _ _ = False

aEquiv : Expr -> Expr -> Bool
aEquiv e1 e2 = aEquivHelper 0 [] e1 [] e2

mutual
  data Neutral
    = NVar Name
    | NApp Neutral Normal
    | NCar Neutral
    | NCdr Neutral
    | NIndNat Neutral Normal Normal Normal
    | NReplace Neutral Normal Normal
    | NIndAbsurd Neutral Normal

  data Normal = Normal' Ty Value

  Env : Type -- Now a type alias
  Env = List (Name,Value)
  %name Env env, env1, env2

  record Closure where
    constructor MkClosure
    closureEnv : Env
    closureName : Name
    closureBody : Expr

  Ty : Type
  Ty = Value

  -- Values
  data Value
    = VPi Ty Closure
    | VLambda Closure
    | VSigma Ty Closure
    | VPair Value Value
    | VNat
    | VZero
    | VAdd1 Value
    | VEq Ty Value Value
    | VSame
    | VTrivial
    | VSole
    | VAbsurd
    | VAtom
    | VTick String
    | VU
    | VNeutral Ty Neutral

extendEnv : Env -> Name -> Value -> Env
extendEnv env x v = ((x, v) :: env)

-- definitions and dependent types
data CtxEntry = Def Ty Value | IsA Ty

Ctx : Type
Ctx = List (Name, CtxEntry)
%name Ctx ctx, ctx1, ctx2

initCtx : Ctx
initCtx = []

ctxNames : Ctx -> List Name
ctxNames ctx = map fst ctx

extendCtx : Ctx -> Name -> Ty -> Ctx
extendCtx ctx x t = (x, (IsA t)) :: ctx

define : Ctx -> Name -> Ty -> Value -> Ctx
define ctx x t v = (x, Def t v) :: ctx

mkEnv : Ctx -> Env
mkEnv [] = []
mkEnv ((x, e) :: ctx) =
  let env = mkEnv ctx in
  (case e of
        (Def _ v) => (x, v) :: env
        (IsA t) => let v = VNeutral t (NVar x) in
                       (x, v) :: env)
-- evaluator
mutual
  data Error
    = MissingValue String
    | CarError
    | CdrError
    | ApplyError
    | IndAbsurdError
    | DoReplaceError
    | DoIndNatError
    | ReadBackTypedError
    | ErrorMessage String

  partial
  evalClosure : Closure -> Value -> Either Error Value
  evalClosure (MkClosure env x e) v =
    eval (extendEnv env x v) e

  evalVar : Env -> Name -> Either Error Value
  evalVar [] x = Left (MissingValue (show x ++ " not found in env"))
  evalVar ((y, v) :: env) x = case x == y of
                                    True => Right v
                                    False => evalVar env x

  partial
  eval : Env -> Expr -> Either Error Value
  eval env (Var x) = evalVar env x
  eval env (Pi x dom ran) =
    do dom' <- eval env dom
       Right (VPi dom' (MkClosure env x ran))
  eval env (Lambda x body) = Right (VLambda (MkClosure env x body))
  eval env (App rator rand) =
    do rator' <- eval env rator
       rand' <- eval env rand
       doApply rator' rand'
  eval env (Sigma x carType cdrType) =
    do carType' <- eval env carType
       Right (VSigma carType' (MkClosure env x cdrType))
  eval env (Cons a d) =
    do a' <- eval env a
       d' <- eval env d
       Right (VPair a' d')
  eval env (Car e) =
    do e' <- eval env e
       doCar e'
  eval env (Cdr e) =
    do e' <- eval env e
       doCdr e'
  eval env Nat = Right VNat
  eval env Zero = Right VZero
  eval env (Add1 e) =
    do e' <- eval env e
       Right (VAdd1 e')
  eval env (IndNat tgt mot base step) =
    do tgt' <- eval env tgt
       mot' <- eval env mot
       base' <- eval env base
       step' <- eval env step
       doIndNat tgt' mot' base' step'
  eval env (Equal ty from to) =
    do ty' <- eval env ty
       from' <- eval env from
       to' <- eval env to
       Right (VEq ty' from' to')
  eval env Same = Right VSame
  eval env (Replace tgt mot base) =
    do tgt' <- eval env tgt
       mot' <- eval env mot
       base' <- eval env base
       doReplace tgt' mot' base'
  eval env Trivial = Right VTrivial
  eval env Sole = Right VSole
  eval env Absurd = Right VAbsurd
  eval env (IndAbsurd tgt mot) =
    do tgt' <- eval env tgt
       mot' <- eval env mot
       doIndAbsurd tgt' mot'
  eval env Atom = Right VAtom
  eval env (Tick x) = Right (VTick x)
  eval env U = Right VU
  eval env (The ty e) = eval env e
  eval env (SrcPos _ e) = eval env e

  -- eliminators
  doCar : Value -> Either Error Value
  doCar (VPair v1 v2) = Right v1
  doCar (VNeutral (VSigma aT dT) neu) =
    Right (VNeutral aT (NCar neu))
  doCar _ = Left CarError

  partial
  doCdr : Value -> Either Error Value
  doCdr (VPair v1 v2) = Right v2
  doCdr v@(VNeutral (VSigma aT dT) neu) =
    do v' <- doCar v
       cl' <- evalClosure dT v'
       Right (VNeutral cl' (NCdr neu))
  doCdr _ = Left CdrError

  partial
  doApply : Value -> Value -> Either Error Value
  doApply (VLambda closure) arg =
    evalClosure closure arg
  doApply (VNeutral (VPi dom ran) neu) arg =
    do arg' <- evalClosure ran arg
       Right (VNeutral arg' (NApp neu (Normal' dom arg)))
  doApply _ _ = Left ApplyError

  doIndAbsurd : Value -> Value -> Either Error Value
  doIndAbsurd (VNeutral VAbsurd neu) mot =
    Right (VNeutral mot (NIndAbsurd neu (Normal' VU mot)))
  doIndAbsurd _ _ = Left IndAbsurdError

  partial
  doReplace : Value -> Value -> Value -> Either Error Value
  doReplace VSame mot base =
    Right base
  doReplace (VNeutral (VEq ty from to) neu) mot base =
    do v' <- doApply mot to
       baseT' <- doApply mot from
       Right (VNeutral v'
         (NReplace neu (Normal' motT mot) (Normal' baseT' base)))
    where
      motT = VPi ty (MkClosure ([]) (Name' "x") U)
  doReplace _ _ _ = Left DoReplaceError

  partial
  indNatStepType : Value -> Either Error Value
  indNatStepType mot =
    eval [(Name' "mot", mot)]
      (Pi (Name' "n-1") Nat
        (Pi (Name' "almost") (App (Var (Name' "mot")) (Var (Name' "n-1")))
          (App (Var (Name' "mot"))
            (Add1 (Var (Name' "n-1"))))))

  partial
  doIndNat : Value -> Value -> Value -> Value -> Either Error Value
  doIndNat VZero mot base step =
    Right base
  doIndNat (VAdd1 v) mot base step =
    do rator' <- (doApply step v)
       rand' <- (doIndNat v mot base step)
       doApply rator' rand'
  doIndNat tgt@(VNeutral VNat neu) mot base step =
    do a' <- (doApply mot tgt)
       b' <- (doApply mot VZero)
       c' <- (indNatStepType mot)
       Right (VNeutral a' (NIndNat neu
         (Normal' (VPi VNat (MkClosure [] (Name' "k") U)) mot) (Normal' b' base)
           (Normal' c' step)))
  doIndNat _ _ _ _ = Left DoIndNatError

-- fresh names

nextName : Name -> Name
nextName (Name' x) = Name' ((show x) ++ "'")

-- could possibly fail for a list like [n', n'', n']
freshen : List Name -> Name -> Name
freshen [] n = n
freshen (x :: used) n = case x == n of
                             False => freshen used n
                             True => freshen used (nextName n)

-- reading back
mutual
  partial
  readBackNeutral : Ctx -> Neutral -> Either Error Expr
  readBackNeutral ctx (NVar x) = Right (Var x)
  readBackNeutral ctx (NApp neu arg) =
    do neu' <- readBackNeutral ctx neu
       arg' <- readBackNormal ctx arg
       Right (App neu' arg')
  readBackNeutral ctx (NCar neu) =
    do car <- readBackNeutral ctx neu
       Right (Car car)
  readBackNeutral ctx (NCdr neu) =
    do cdr <- readBackNeutral ctx neu
       Right (Cdr cdr)
  readBackNeutral ctx (NIndNat neu mot base step) =
    do neu' <- readBackNeutral ctx neu
       mot' <- readBackNormal ctx mot
       base' <- readBackNormal ctx base
       step' <- readBackNormal ctx step
       Right (IndNat neu' mot' base' step')
  readBackNeutral ctx (NReplace neu mot base) =
    do neu' <- readBackNeutral ctx neu
       mot' <- readBackNormal ctx mot
       base' <- readBackNormal ctx base
       Right (Replace neu' mot' base')
  readBackNeutral ctx (NIndAbsurd neu mot) =
    do neu' <- readBackNeutral ctx neu
       mot' <- readBackNormal ctx mot
       Right (IndAbsurd (The Absurd neu') mot')

  partial
  readBackTyped : Ctx -> Ty -> Value -> Either Error Expr
  readBackTyped ctx VNat VZero = Right Zero
  readBackTyped ctx VNat (VAdd1 v) =
    do n <- (readBackTyped ctx VNat v)
       Right (Add1 n)
  readBackTyped ctx (VPi dom ran) fun =
    let x = freshen (ctxNames ctx) (closureName ran)
        xVal = VNeutral dom (NVar x)
        ctx' = extendCtx ctx x dom in
    do ty' <- evalClosure ran xVal
       v' <- doApply fun xVal
       body <- readBackTyped ctx' ty' ty'
       Right (Lambda x body)
  readBackTyped ctx (VSigma aT dT) pair =
    do carVal <- doCar pair
       car <- readBackTyped ctx aT carVal
       cdrT <- evalClosure dT carVal
       cdrVal <- doCdr pair
       cdr <- readBackTyped ctx cdrT cdrVal
       Right (Cons car cdr)
  readBackTyped ctx VAbsurd (VNeutral VAbsurd neu) =
    do a <- readBackNeutral ctx neu
       Right (The Absurd a)
  readBackTyped ctx (VEq _ _ _) VSame = Right Same
  readBackTyped ctx VAtom (VTick x) = Right (Tick x)
  readBackTyped ctx VU VNat = Right Nat
  readBackTyped ctx VU VAtom = Right Atom
  readBackTyped ctx VU VTrivial = Right Trivial
  readBackTyped ctx VU VAbsurd = Right Absurd
  readBackTyped ctx VU (VEq t from to) =
    do a <- readBackTyped ctx VU t
       b <- readBackTyped ctx t from
       c <- readBackTyped ctx t to
       Right (Equal a b c)
  readBackTyped ctx VU (VSigma aT dT) =
    let x = freshen (ctxNames ctx) (closureName dT) in
        do a <- readBackTyped ctx VU aT
           body <- evalClosure dT (VNeutral aT (NVar x))
           d <- readBackTyped (extendCtx ctx x aT) VU body
           Right (Sigma x a d)
  readBackTyped ctx VU (VPi aT bT) =
    let x = freshen (ctxNames ctx) (closureName bT) in
        do a <- readBackTyped ctx VU aT
           body <- evalClosure bT (VNeutral aT (NVar x))
           b <- readBackTyped (extendCtx ctx x aT) VU body
           Right (Pi x a b)
  readBackTyped ctx VU VU = Right U
  readBackTyped ctx t (VNeutral t' neu) = readBackNeutral ctx neu
  readBackTyped _ otherT otherE = Left ReadBackTypedError

  partial
  readBackNormal : Ctx -> Normal -> Either Error Expr
  readBackNormal ctx (Normal' t v) = readBackTyped ctx t v

-- helpers
lookupType : Ctx -> Name -> Either Error Ty -- didn't use message type
lookupType [] x = Left (ErrorMessage "unbound variable: ") -- TODO ++ show x
lookupType ((y, e) :: ctx) x =
  (case x == y of
        False => lookupType ctx x
        True => (case e of
                      (Def t _) => Right t
                      (IsA t) => Right t))

unexpected : Ctx -> String -> Value -> Either Error a

isPi : Ctx -> Value -> Either Error (Ty, Closure)
isPi _ (VPi a b) = Right (a, b)
isPi ctx other = unexpected ctx "Not a Pi type" other

isSigma : Ctx -> Value -> Either Error (Ty, Closure)
isSigma _ (VSigma a b) = Right (a, b)
isSigma ctx other = unexpected ctx "Not a Sigma type" other

isNat : Ctx -> Value -> Either Error ()
isNat _ VNat = Right ()
isNat ctx other = unexpected ctx "Not Nat" other

isEqual : Ctx -> Value -> Either Error (Ty, Value, Value)
isEqual _ (VEq ty from to) = Right (ty, from, to)
isEqual ctx other = unexpected ctx "Not an equality type" other

isAbsurd : Ctx -> Value -> Either Error ()
isAbsurd _ VAbsurd = Right ()
isAbsurd ctx other = unexpected ctx "Not Absurd: " other

isTrivial : Ctx -> Value -> Either Error ()
isTrivial _ VTrivial = Right ()
isTrivial ctx other = unexpected ctx "Not Trivial" other

isAtom : Ctx -> Value -> Either Error ()
isAtom _ VAtom = Right ()
isAtom ctx other = unexpected ctx "Not Atom" other

-- checking/synthesis
mutual
  partial
  check : Ctx -> Expr -> Ty -> Either Error ()
  check ctx (Lambda x body) t = ?check_rhs_3
  check ctx (Cons a d) t = ?check_rhs_6
  check ctx Zero t = isNat ctx t
  check ctx (Add1 n) t = do
    isNat ctx t
    check ctx n VNat
  check ctx Same t = do
    (t, from, to) <- isEqual ctx t
    convert ctx t from to
  check ctx Sole t = isTrivial ctx t
  check ctx (Tick x) t = isAtom ctx t
  check ctx other t = do
    t' <- synth ctx other
    convert ctx VU t' t

  convert : Ctx -> Ty -> Value -> Value -> Either Error ()

  partial
  synth : Ctx -> Expr -> Either Error Ty
  synth ctx (Var x) = lookupType ctx x
  synth ctx (Pi x a b) =
    do check ctx a VU
       v <- eval (mkEnv ctx) a
       check (extendCtx ctx x v) b VU
       Right VU
  synth ctx (App rator rand) =
    do funTy <- synth ctx rator
       (a, b) <- isPi ctx funTy
       check ctx rand a
       body <- eval (mkEnv ctx) rand
       evalClosure b body
  synth ctx (Sigma x a b)
    = do check ctx a VU
         a' <- eval (mkEnv ctx) a
         check (extendCtx ctx x a') b VU
         Right VU
  synth ctx (Car e) =
    do t <- synth ctx e
       (aT, dT) <- isSigma ctx t
       Right aT
  synth ctx (Cdr e) =
    do t <- synth ctx e
       (aT, dT) <- isSigma ctx t
       e' <- eval (mkEnv ctx) e
       body <- doCar e'
       evalClosure dT body
  synth ctx Nat = Right VU
  synth ctx (IndNat tgt mot base step)
    = do t <- synth ctx tgt
         tgtV <- eval (mkEnv ctx) tgt
         motTy <- eval (mkEnv []) (Pi (Name' "x") Nat U)
         check ctx mot motTy
         motV <- eval (mkEnv ctx) mot
         z' <- doApply motV VZero
         check ctx base z'
         m' <- indNatStepType motV
         check ctx step m'
         doApply motV tgtV
  synth ctx (Equal ty from to)
    = do check ctx ty VU
         tyV <- eval (mkEnv ctx) ty
         check ctx from tyV
         check ctx to tyV
         Right VU
  synth ctx (Replace tgt mot base)
    = do t <- synth ctx tgt
         (ty, from, to) <- isEqual ctx t
         motTy <- eval ([(Name' "ty", ty)]) (Pi (Name' "x") (Var (Name' "ty")) U)
         check ctx mot motTy
         motV <- eval (mkEnv ctx) mot
         fromV <- doApply motV from
         check ctx base fromV
         doApply motV to
  synth ctx Trivial = Right VU
  synth ctx Absurd = Right VU
  synth ctx (IndAbsurd tgt mot)
    = do t <- synth ctx tgt
         isAbsurd ctx t
         check ctx mot VU
         eval (mkEnv ctx) mot
  synth ctx Atom = Right VU
  synth ctx U = Right VU
  synth ctx (The ty expr)
    = do check ctx ty VU
         tyV <- eval (mkEnv ctx) ty
         check ctx expr tyV
         Right tyV
  synth ctx other = Left (ErrorMessage "Unable to synthesize a type for ") -- ++ show other

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
> module SequentialDecisionProblems.examples.Main

> import Decidable.Order

> import Data.List
> import Data.List.Quantifiers
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.NonDeterministicDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.ViabilityDefaults

> import SequentialDecisionProblems.examples.LeftAheadRight

> import List.Operations
> import List.Properties
> import BoundedNat.BoundedNat
> import BoundedNat.Operations
> import BoundedNat.Properties
> import Sigma.Sigma
> import Nat.LTEProperties
> import Nat.LTProperties
> import Nat.OperationsProperties
> import LocalEffect.Exception
> import LocalEffect.StdIO

> -- %default total
> %auto_implicits off

> -- %logging 5

We reimplement "Example1.lidr", this time with |M = List|.

* The decision process:

> maxColumn : Nat
> maxColumn = 10

> nColumns : Nat
> nColumns = S maxColumn

** States:

> SequentialDecisionProblems.CoreTheory.State t = LTB nColumns

** Controls:

> SequentialDecisionProblems.CoreTheory.Ctrl t x = LeftAheadRight

** Transition function:

> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma Z prf) Left =
>   [MkSigma maxColumn (ltIdS maxColumn)]
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma (S n) prf) Left =
>   [MkSigma n (ltLemma1 n nColumns prf)]
> SequentialDecisionProblems.CoreTheory.nexts t x Ahead = [x]
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma n prf) Right with (decLT n maxColumn)
>   | (Yes p)     = [MkSigma (S n) (LTESucc p)]
>   | (No contra) = [MkSigma  Z    (LTESucc LTEZero)]

** |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   Nat

> SequentialDecisionProblems.CoreTheory.plus =
>   Prelude.Nat.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   Z

> SequentialDecisionProblems.CoreTheory.LTE =
>   Prelude.Nat.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   Nat.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   Nat.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   Nat.LTEProperties.monotoneNatPlusLTE

> SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE =
>   Nat.LTEProperties.totalPreorderLTE

** Reward function:

> SequentialDecisionProblems.CoreTheory.reward t x y (MkSigma c _) =
>   if c == Z
>   then (S Z)
>   else if (S c) == nColumns
>        then (S (S Z))
>        else Z

** Measure:

> SequentialDecisionProblems.CoreTheory.meas = sum
> SequentialDecisionProblems.FullTheory.measMon = sumMon

** |Ctrl| is finite:

> SequentialDecisionProblems.Utils.finiteCtrl _ =
>   finiteLeftAheadRight

** Reachability

> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (xs : List (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) xs
>   all Nil = Nil
>   all (x :: xs) = () :: (all xs)

* The computation:

> SequentialDecisionProblems.Utils.showState = show @{ShowLTB}
> SequentialDecisionProblems.Utils.showCtrl = show

> computation : { [STDIO] } Eff ()
> computation =
>   do putStr ("enter number of steps:\n")
>      nSteps <- getNat
>      putStr ("enter initial column:\n")
>      x0 <- getLTB nColumns
>      case (decidableViable {t = Z} nSteps x0) of
>        (Yes v0) => do putStrLn ("computing optimal policies ...")
>                       ps   <- pure (backwardsInduction Z nSteps)
>                       putStrLn ("computing optimal controls ...")
>                       mxys <- pure (possibleStateCtrlSeqs x0 () v0 ps)
>                       putStrLn (show mxys)
>                       putStrLn ("done!")
>        (No _)   => putStrLn ("initial column non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> {-

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.List.Views

total
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix xs ys with (snocList xs)
  equalSuffix [] ys | Empty = []
  equalSuffix (zs ++ [x]) ys | (Snoc rec) with (snocList ys)
    equalSuffix (xs' ++ [x]) [] | (Snoc rec) | Empty = []
    equalSuffix (xs' ++ [x]) (ys' ++ [y]) | (Snoc rec_xs) | (Snoc rec_ys)
      = if x == y
        then (equalSuffix xs' ys' | rec_xs | rec_ys) ++ [x]
        else []

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
||| Fibonacci but in linear time
module Main
import Cairo

-- O(n) version
fibl : Felt -> Felt
fibl n = go n 0 1
  where
    go : Felt -> Felt -> Felt -> Felt
    go n a b = if n == 0 then a else go (n-1) b (a+b)

%noinline
main : Cairo ()
main = output (fibl 10)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro