git.iko.soy/Idris-dev
on master help sign in
Rewrite ForeignTy as non-tail-recursive to simplify proving equality
6cdb125Benjamin Saunders
lib/IO.idr+2−4
compare with master
unifiedsplit
@@ -33,10 +33,8 @@ interpFTy (FAny t) = t
33interpFTy FUnit = ()
33interpFTy FUnit = ()
34
34
35ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
35ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
36−ForeignTy xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where
36+ForeignTy Nil rt = IO (interpFTy rt)
37− mkForeign' : List FTy -> Type -> Type
37+ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
38− mkForeign' Nil ty = ty
39− mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
40
38
41
39
42data Foreign : Type -> Type where
40data Foreign : Type -> Type where