Final stuff on SystemF

SystemF/Comble.hs

@@ -80,4 +80,4 @@ termsOfSize n = memoGo (n,0) where
   go (s+1,m) =
        asum [pure (Var v) | v <- [0..m-1]]
    <|> (Lam <$> go (s,m+1))
-   <|> asum [ pure Apply <*> go (s1,m) <*> go (s2, m) | (s1, s2) <- split2 s]
+   <|> asum [ pure Apply <*> memoGo (s1,m) <*> memoGo (s2, m) | (s1, s2) <- split2 s]

SystemF/check.hs

@@ -144,3 +144,7 @@ hackyextract (Left s) = undefined
 testsubs :: Comble Type -> [(Type, Type, (Type, Type))]
 testsubs tys = filter (\(a,b,c) -> a /= b) [(ty, (uncurry reconstruct) pair, pair) | ty <- toList $ tys, pair <- allsubstitutions ty]
 
+-- Test whether generated terms are of the intended type
+testgenterm :: Type -> Env -> Int -> Int -> [(Either String Type, Term)]
+testgenterm ty env nte nty = filter (\(t, _) -> Right ty /= t) $ map (\t -> (typeOf t env, t)) $ toList $ termoftype ty env nte nty
+