# Verify Idris 2 toolchain
command -v idris2 >/dev/null || exit 11

# Verify Idris artifacts exist
fd -e ipkg -e idr . >/dev/null || exit 12

PLAN -> CREATE -> VERIFY -> REMEDIATE
  |        |         |          |
  v        v         v          v
Design  Generate   Check     Complete
Types   .idr      Totality   Holes

DEFINE -> REFINE -> PROVE -> CHECK -> IMPLEMENT
    ^                                      |
    +--------------------------------------+

1. DEFINE: Write type signatures with holes
2. REFINE: Use hole-driven development to explore types
3. PROVE: Fill holes with total implementations
4. CHECK: `idris2 --check` to verify totality
5. IMPLEMENT: Extract verified components

Use sequential-thinking for:
- Type-level encoding strategy
- Totality proof planning
- Function coverage analysis

Use actor-critic-thinking for:
- Type design alternatives
- Dependent type trade-offs
- Proof complexity evaluation

Use shannon-thinking for:
- Type-level property coverage
- Holes requiring completion
- Totality risk assessment

-- Target: .outline/proofs/{Module}.idr
module {Module}

%default total

{-
From requirement: {requirement text}

Properties encoded in types:
- Property 1: {how encoded}
- Property 2: {how encoded}
-}

-- Dependent type encoding invariant
data ValidState : (n : Nat) -> Type where
  MkValid : (prf : n > 0) -> ValidState n

-- From requirement: {requirement text}
-- Total function with type-level proof
processValid : ValidState n -> ValidState (n + 1)
processValid (MkValid prf) = MkValid ?proof_todo

-- Covering function ensuring all cases handled
covering
handleAll : Either a b -> Result
handleAll (Left x) = ?left_case
handleAll (Right y) = ?right_case

-- Type-level proof
lemma_property : (x : Nat) -> (y : Nat) -> x + y = y + x
lemma_property x y = ?commutativity_proof

# Create .outline/proofs directory for Idris files
mkdir -p .outline/proofs

-- .outline/proofs/{Module}.idr
-- Generated from plan design

module {Module}

%default total

{-
Source Requirements: {traceability from plan}

Properties Encoded in Types:
- Property 1: {how encoded from plan}
- Property 2: {how encoded from plan}
-}

-- === Dependent Types from Plan ===

-- Type encoding invariant: {from plan design}
public export
data ValidState : (n : Nat) -> Type where
  MkValid : (prf : n > 0 = True) -> ValidState n

-- Type encoding constraint: {from plan design}
public export
data Bounded : (lower : Nat) -> (upper : Nat) -> (n : Nat) -> Type where
  MkBounded : (prf : (lower <= n && n <= upper) = True) -> Bounded lower upper n

-- === Functions with Type-Level Proofs ===

-- From requirement: {requirement text}
-- Total function with type-level proof
public export
processValid : ValidState n -> ValidState (S n)
processValid (MkValid prf) = MkValid ?proof_valid_successor

-- Covering function ensuring all cases handled
public export covering
handleAll : Either a b -> (a -> c) -> (b -> c) -> c
handleAll (Left x) f g = f x
handleAll (Right y) f g = g y

-- === Type-Level Proofs ===

-- Lemma: {property from plan}
public export
lemma_property : (x : Nat) -> (y : Nat) -> x + y = y + x
lemma_property x y = ?commutativity_proof

-- .outline/proofs/{package}.ipkg
-- Generated from plan design

package {package_name}

sourcedir = "."

modules = {Module1}, {Module2}

depends = base, contrib

# Verify Idris 2 availability
command -v idris2 >/dev/null || exit 11

# Verify artifacts exist
fd -e idr -e ipkg .outline/proofs >/dev/null || exit 12

# Package build
fd -e ipkg .outline/proofs -x idris2 --build {} || exit 13

# Direct file check
fd -e idr .outline/proofs -x idris2 --check {} || exit 13

# Check totality (all functions terminate)
fd -e idr .outline/proofs -x idris2 --total {} || exit 14

# Find incomplete holes
HOLES=$(rg -c '\?\w+' .outline/proofs/ || echo "0")
echo "Holes remaining: $HOLES"

# Check for partial annotations
rg -n 'partial\s+\w+|covering\s+\w+' .outline/proofs/ && {
  echo "Warning: partial/covering functions found"
}

-- Before (with hole)
processValid : ValidState n -> ValidState (S n)
processValid (MkValid prf) = MkValid ?proof_valid_successor

-- After (hole filled)
processValid : ValidState n -> ValidState (S n)
processValid (MkValid prf) = MkValid Refl

-- Before (partial)
partial
unsafeHead : List a -> a
unsafeHead (x :: _) = x

-- After (total with proof)
total
safeHead : (xs : List a) -> {auto prf : NonEmpty xs} -> a
safeHead (x :: _) = x

# Check single file
idris2 --check src/Main.idr

# Build package
idris2 --build project.ipkg

# Build with timing info
idris2 --build project.ipkg --timing

# Interactive REPL
idris2 src/Main.idr

# Generate documentation
idris2 --mkdoc project.ipkg

# Install package
idris2 --install project.ipkg

# Clean build artifacts
idris2 --clean project.ipkg

# Check totality explicitly
idris2 --total --check src/Main.idr

# List installed packages
idris2 --list-packages

# Full verification
idris2 --build project.ipkg && rg 'maybe not total\|covering' . && exit 14 || echo "All types verified"

-- Length-indexed vectors
data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect n a -> Vect (S n) a

-- Finite numbers (bounded indices)
data Fin : Nat -> Type where
  FZ : Fin (S n)           -- Zero is valid for any non-empty range
  FS : Fin n -> Fin (S n)  -- Successor preserves bound

-- Decidable propositions
data Dec : Type -> Type where
  Yes : p -> Dec p         -- Proof that p holds
  No  : Not p -> Dec p     -- Proof that p doesn't hold

-- Dependent pairs (existentials)
data DPair : (a : Type) -> (p : a -> Type) -> Type where
  MkDPair : (x : a) -> p x -> DPair a p

-- Syntax sugar for dependent pairs
(n ** Vect n a)  -- equivalent to DPair Nat (\n => Vect n a)

-- Subset types (refinements)
data Subset : Type -> (pred : a -> Type) -> Type where
  Element : (x : a) -> pred x -> Subset a pred

-- Boolean reflection
data So : Bool -> Type where
  Oh : So True

> :prove myHole
--------------------
Goal: Vect (n + m) a

> intro xs        -- Introduce variable
> intros          -- Introduce all
> exact e         -- Provide exact term
> refine f        -- Apply function
> trivial         -- Solve trivial goal
> search          -- Auto-search for proof
> qed             -- Complete proof

-- Mark function as total (compiler verifies)
total
append : Vect n a -> Vect m a -> Vect (n + m) a

-- Mark as partial (explicit escape hatch)
partial
infiniteLoop : a -> b

-- Mark as covering (all cases handled but may not terminate)
covering
process : Stream a -> IO ()

-- Idris infers termination from structural recursion
total
length : Vect n a -> Nat
length [] = 0
length (x :: xs) = 1 + length xs

-- For complex recursion, use sized types or well-founded recursion
total
merge : Ord a => List a -> List a -> List a
merge [] ys = ys
merge xs [] = xs
merge (x :: xs) (y :: ys) =
  if x <= y
    then x :: merge xs (y :: ys)
    else y :: merge (x :: xs) ys

-- src/Data/SafeList.idr

module Data.SafeList

import Data.Vect
import Data.Fin

%default total

||| A non-empty list with type-level length guarantee
public export
data SafeList : Nat -> Type -> Type where
  Singleton : a -> SafeList 1 a
  Cons : a -> SafeList n a -> SafeList (S n) a

||| Safe head - always succeeds on non-empty list
export
head : SafeList (S n) a -> a
head (Singleton x) = x
head (Cons x _) = x

||| Safe index - type guarantees bounds
export
index : Fin n -> SafeList n a -> a
index FZ (Singleton x) = x
index FZ (Cons x _) = x
index (FS i) (Cons _ xs) = index i xs

||| Filter with proof of length relationship
filter : (a -> Bool) -> Vect n a -> (m ** Vect m a)
filter p [] = (0 ** [])
filter p (x :: xs) =
  let (m ** xs') = filter p xs in
  if p x
    then (S m ** x :: xs')
    else (m ** xs')

||| Usage: pattern match to extract length and vector
processFiltered : Vect n Nat -> IO ()
processFiltered xs =
  let (m ** ys) = filter (> 5) xs in
  putStrLn $ "Kept " ++ show m ++ " elements"

||| Door state encoded in types
data DoorState = Open | Closed

||| Door operations indexed by state transitions
data Door : DoorState -> Type where
  MkDoor : Door Closed

||| Type-safe operations
openDoor : Door Closed -> Door Open
openDoor MkDoor = ?openDoor_rhs  -- Implementation

closeDoor : Door Open -> Door Closed
closeDoor d = ?closeDoor_rhs

||| Cannot close an already closed door - type error!
-- closeDoor MkDoor  -- Won't compile

Scenario                           -> Type Construct
-------------------------------------------------------------
Length known at compile-time       -> Vect n a
Safe array indexing (0 to n-1)     -> Fin n
Decidable proposition with proof   -> Dec p
Unknown-length result (filtering)  -> DPair a p (dependent pair)
Refined type with proof            -> Subset a p
Convert Bool to Type               -> So b
Prove element in collection        -> Elem x xs
Non-empty guarantee                -> List1 a or (xs : List a ** NonEmpty xs)
Bounded numeric range              -> data InRange : (lo : Nat) -> (hi : Nat) -> Type

processData : (input : ValidInput) -> {auto prf : IsPositive (value input)} -> Result
processData input = ?processData_impl

idris2 --check Module.idr
# Output shows: processData_impl : Result

:t processData_impl     -- Show type of hole
:doc Result             -- Documentation for type
:search Nat -> Bool     -- Find functions matching signature
:prove processData_impl -- Interactive proof mode (if available)

-- Before
processData input = ?processData_impl

-- After case split
processData (MkValidInput val prf) = ?processData_impl_1

-- Continue refining
processData (MkValidInput val prf) = MkResult (compute val)

# Check single file
idris2 --check Module.idr

# Check with totality enforcement
idris2 --total Module.idr

# Build package
idris2 --build package.ipkg

# REPL for interactive exploration
idris2 Module.idr
# Then use :t, :doc, :search commands

# Find all holes
rg '\?\w+' .outline/proofs/

# Find partial/covering annotations
rg 'partial|covering' .outline/proofs/

# Check what's exported
idris2 --check Module.idr --show-exports

# Verbose compilation
idris2 --check --verbose Module.idr

-- Problematic: structural recursion not obvious
loop : List Nat -> Nat
loop [] = 0
loop (x :: xs) = x + loop (filter (< x) xs)  -- filter result size unknown

-- Solution 1: Use sized types / assert_smaller
loop (x :: xs) = x + loop (assert_smaller (x :: xs) (filter (< x) xs))

-- Solution 2: Use Nat-indexed recursion
loopN : (fuel : Nat) -> List Nat -> Nat
loopN Z _ = 0
loopN (S k) [] = 0
loopN (S k) (x :: xs) = x + loopN k (filter (< x) xs)

-- Incomplete
process : Either a b -> c
process (Left x) = handleLeft x
-- Missing: process (Right y) = ...

-- Complete
process : Either a b -> c
process (Left x) = handleLeft x
process (Right y) = handleRight y

-- Problem: filter returns unknown length
filterPositive : Vect n Int -> Vect ? Int  -- Can't know output length

-- Solution: Use dependent pair
filterPositive : Vect n Int -> (m : Nat ** Vect m Int)
filterPositive [] = (0 ** [])
filterPositive (x :: xs) =
  let (m ** rest) = filterPositive xs
  in if x > 0 then (S m ** x :: rest) else (m ** rest)

-- Alternative: Use List for variable-length, prove properties
filterPositiveList : List Int -> (xs : List Int ** All (\x => x > 0) xs)

-- Proof arguments erased at runtime (0 multiplicity)
safeHead : (xs : List a) -> {0 prf : NonEmpty xs} -> a
safeHead (x :: _) = x

-- Runtime-relevant (1 multiplicity, default)
process : (n : Nat) -> Vect n a -> a
process (S _) (x :: _) = x

-- Unrestricted (can use multiple times)
duplicate : {w : _} -> a -> (a, a)
duplicate x = (x, x)

-- Bad: Idris can't see termination
ackermann : Nat -> Nat -> Nat
ackermann Z n = S n
ackermann (S m) Z = ackermann m 1
ackermann (S m) (S n) = ackermann m (ackermann (S m) n)

-- Good: Use sized types or assert_total with proof
total
ackermann : Nat -> Nat -> Nat
ackermann Z n = S n
ackermann (S m) Z = ackermann m 1
ackermann (S m) (S n) = assert_total $ ackermann m (ackermann (S m) n)
-- Note: assert_total should be justified with external proof

-- Bad: Proof carried at runtime
data Positive : Nat -> Type where
  IsPos : (n : Nat) -> Positive (S n)

-- Good: Use 0-quantity for erased proofs
data Positive : Nat -> Type where
  IsPos : (0 n : Nat) -> Positive (S n)
  -- The `0` means n is erased at runtime

-- Bad: Loses length information
filterBad : (a -> Bool) -> Vect n a -> List a

-- Good: Use dependent pair to preserve relationship
filter : (a -> Bool) -> Vect n a -> (m ** Vect m a)

-- Or use decidable predicates
filterDec : (p : a -> Bool) ->
            Vect n a ->
            (m ** (Vect m a, (x : a) -> Elem x result -> So (p x)))

-- Bad: Ambiguous implicit
append xs ys = ?hole

-- Good: Explicit type annotation
append : {n, m : Nat} -> Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

-- Or provide implicits at call site
result = append {n = 3} {m = 2} xs ys

-- SLOW: Proof computed at runtime
slowHead : (xs : List a) -> {auto prf : NonEmpty xs} -> a

-- FAST: Proof erased
fastHead : (xs : List a) -> {auto 0 prf : NonEmpty xs} -> a

-- Strict evaluation (default)
data Tree a = Leaf | Node a (Tree a) (Tree a)

-- Lazy evaluation for infinite/large structures
data LazyTree a = Leaf | Node a (Lazy (LazyTree a)) (Lazy (LazyTree a))

-- SLOW: Unary Nat arithmetic
slowAdd : Nat -> Nat -> Nat
slowAdd Z m = m
slowAdd (S n) m = S (slowAdd n m)

-- FAST: Use Integer primitives
fastAdd : Integer -> Integer -> Integer
fastAdd = (+)