Co-natural deduction

Coterm.idr

-- Greatest fixpoint of (1 + a * x), "possibly-terminating streams"
data Colist : Type -> Type where 
  Nil : Colist a 
  (::) : a -> Inf (Colist a) -> Colist a 

-- Environment indexed by a colist
data CoAll : (p : k -> Type) -> Colist k -> Type where 
  Empty : CoAll p Nil
  Cons : {p : k -> Type} -> p x -> Inf (CoAll p xs) -> CoAll p (x :: xs)

-- Terms indexed by an output stack of variables
data Coterm : Ty -> Colist Ty -> Type where 
  MatR : Coterm g (a::d) -> Coterm g (b::d) -> Coterm g (With a b :: d)
  Prjl : Coterm a d -> Coterm (With a b) d
  Prjr : Coterm b d -> Coterm (With a b) d

-- Evaluate a term and a value and generate a lazy stack of variables
evalco : Coterm t ctx -> Val t -> CoAll Val ctx
evalco (MatR t1 t2) v = let Cons a env = evalco t1 v 
                            Cons b env = evalco t2 v in Cons (a, b) env
evalco (Prjl t) (v1, _) = evalco t v1
evalco (Prjr t) (_, v2) = evalco t v2