demo.ii

-- let-bound mixfix not in scope
-- poly1 = let _<_ = \f a => f a in (\y => y . t) < { t = 1 }  -- %i1

-- Illegal pattern (multi-line equation)
-- eq1 @x b = 2
-- eq1 a b = 3

-- multi-branch μ merge =>
-- rec1 v = { a = rec1 v , b = rec1 v }  -- ∏ A B → ⊤ → µa.{a : a , b : a}

-- Add Module names to namespace , name clash when opening ?
-- import Maybe
-- y = Maybe

--imports list list2 tree question ls foldr Free parsec intmap patternTests hash
--import irieShell -- ideas for irie as shell
--import imports/TreeStream
--import SpecialisationTests/{SpecPapArg , SimpleMutual , SumOfSquares , fib , WrappedSimpleMutual}
--import SpecTests
--import testBruijns -- β-reduction
--import testFuse
--import sumMul
--import letCaptureTests
--import casecase
--import tupleTests
--import Tee -- duplicate streams
--import dir
--import asmTests
--import ii/Subsumption
--import CTests

-- Captures VQBindIndex{} on use before declare
--x = Just 3
--Maybe = data
--  Just Int
-- x = Just 3 -- ok

-- Allow declaring recursive data types; μ?
--IntList = data
--  Nil
--  Cons Int -- IntList
--g (Cons x) = x
--f = Cons 3

-- type params (conv BruijnAbs to THBi)
-- * Bruijns in types are already THBounds
-- ? type application vs implicit
-- Maybe a = data
--   Nothing
--   Just a
-- f = Just 3

-- funArg (& polys)
-- foldr f s l = add 0 case l of
--  @Cons x xs => f (add 0 x) (foldr f s xs)
--  @Nil       => add s 0

-- lift labels so can be imported with type / fwd reffed etc..
-- import m2
-- f = d1 -- imported label (& fwd refs to labels)

-- * Type application (& type params) & Cast to TPoly
-- * Specialise polys to a size
-- id x = x
-- f = id 3

-- ? where to alloc mem. Stack is good iff mem is freed on same stack frame
-- withAlloca : ∀a. Int -> IO ()
-- unfoldrStr : (seed -> Next a seed) -> seed -> Array a

-- * Alt casts infer:409
-- altCast e = case e of
--   True  => { x = 0 } -- i1 <: i8
--   False => { x = 5 } -- i8

-- Post-infer casts
-- ! If contains tvars, can save up/lo bounds to bind; Can tvars change casts from above the term?
-- eg. either = \case {Left a => a ; Right a => add a 3 }
--  : "Either A Int -> Int ⊔ A"
-- A between [⊥ , Int]; infer can't cast it because depends on tvar bounds.
--either = \case
--  @Left a  => add a 2
--  @Right b => add b 5
-- main = either (@Left 3)

-- lift / inline / specialise bruijn fns & η-expand paps
-- Paps are specialisations, lambdas can be lifted by parser
-- ap f x = f x
-- main = ap (\y => add 3 y) 4

--import subsume.ii
--import stream

-- No β-reduce duplicates ; 0-arity dup/let-bind eg.
-- main = (\x => add x x) (add 3 2)

--f = \x => \y => add x y
--f = let f0 x = let f1 y = add x y in f1 in f0

-- TODO separate pass for casting, incl type application