Fix SystemFImpl and update SystemFBase

SystemF/SystemFBase.hs

@@ -82,19 +82,15 @@ freeVariablesType c (TyBase) = (nub (concat [[]]))
 
 termOfSize env 0 nType = (empty)
 termOfSize env 1 nType = (TmVar <$> (getTermVar env (Z)))
-termOfSize env nTerm nType = ((TmAbs <$> (termOfSize (termEnv (STermVar env)) (nTerm - 1) nType) <*> (typeUpToSize env nType))
+termOfSize env nTerm nType = ((TmAbs <$> (termOfSize (STermVar env) (nTerm - 1) nType) <*> (typeUpToSize env nType))
                               <|> (asum (map (\l -> (TmApp <$> (termOfSize env ((!!) l 0) nType) <*> (termOfSize env ((!!) l 1) nType))) (splitn 2 (nTerm - 1))))
                               <|> (TmTApp <$> (termOfSize env (nTerm - 1) nType) <*> (typeUpToSize env nType))
-                              <|> (TmTAbs <$> (termOfSize (termEnv (STypeVar env)) (nTerm - 1) nType)))
+                              <|> (TmTAbs <$> (termOfSize (STypeVar env) (nTerm - 1) nType)))
 
 termUpToSize env 0 nType = (empty)
 termUpToSize env nTerm nType = ((termUpToSize env (nTerm - 1) nType)
                                 <|> (termOfSize env nTerm nType))
 
-termEnv (STermVar next) = (STermVar (termEnv next))
-termEnv (STypeVar next) = (STypeVar (termEnv next))
-termEnv (Z) = (Z)
-
 forTermWithSize env nTerm nType prop = (let c = (termOfSize env nTerm nType)
                                             n = (card c)
                                             g = ((Comble.!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
@@ -104,16 +100,12 @@ typeOfSize env 0 = (empty)
 typeOfSize env 1 = ((TyVar <$> (getTypeVar env (Z)))
                     <|> (pure TyBase))
 typeOfSize env nType = ((asum (map (\l -> (TyArr <$> (typeOfSize env ((!!) l 0)) <*> (typeOfSize env ((!!) l 1)))) (splitn 2 (nType - 1))))
-                        <|> (TyAll <$> (typeOfSize (typeEnv (STypeVar env)) (nType - 1))))
+                        <|> (TyAll <$> (typeOfSize (STypeVar env) (nType - 1))))
 
 typeUpToSize env 0 = (empty)
 typeUpToSize env nType = ((typeUpToSize env (nType - 1))
                           <|> (typeOfSize env nType))
 
-typeEnv (STypeVar next) = (STypeVar (typeEnv next))
-typeEnv (STermVar next) = (typeEnv next)
-typeEnv (Z) = (Z)
-
 forTypeWithSize env nType prop = (let c = (typeOfSize env nType)
                                       n = (card c)
                                       g = ((Comble.!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
@@ -123,17 +115,13 @@ genInt = (asum [(pure 0),(pure 1),(pure 2),(pure 3)])
 
 genString = (asum [(pure "a"),(pure "b"),(pure "c"),(pure "d")])
 
-reverseVar (Z) res = res
-reverseVar (STermVar next) res = (reverseVar next (STermVar res))
-reverseVar (STypeVar next) res = (reverseVar next (STypeVar res))
-
 getTermVar (Z) _ = (empty)
-getTermVar (STermVar next) abs = ((pure (reverseVar abs (Z)))
+getTermVar (STermVar next) abs = ((pure abs)
                                   <|> (getTermVar next (STermVar abs)))
 getTermVar (STypeVar next) abs = (getTermVar next (STypeVar abs))
 
 getTypeVar (Z) _ = (empty)
-getTypeVar (STypeVar next) abs = ((pure (reverseVar abs (Z)))
+getTypeVar (STypeVar next) abs = ((pure abs)
                                   <|> (getTypeVar next (STypeVar abs)))
 getTypeVar (STermVar next) abs = (getTypeVar next (STermVar abs))
 
@@ -181,10 +169,10 @@ memoTerm env nTe nType = memo env nTe
     go :: Variable -> Integer -> Comble Term
     go env 0     = (empty)
     go env 1     = (TmVar <$> (getTermVar env (Z)))
-    go env nTerm = ((TmAbs <$> (memo (termEnv (STermVar env)) (nTerm - 1)) <*> (typeUpToSize env nType))
+    go env nTerm = ((TmAbs <$> (memo ((STermVar env)) (nTerm - 1)) <*> (typeUpToSize env nType))
                <|> (asum (map (\l -> (TmApp <$> (memo env ((!!) l 0)) <*> (memo env ((!!) l 1)))) (splitn 2 (nTerm - 1))))
                <|> (TmTApp <$> (memo env (nTerm - 1)) <*> (typeUpToSize env nType))
-               <|> (TmTAbs <$> (memo (termEnv (STypeVar env)) (nTerm - 1))))
+               <|> (TmTAbs <$> (memo ((STypeVar env)) (nTerm - 1))))
 
 forMemoTermWithSize env nTerm nType prop = (let c = (memoTerm env nTerm nType)
                                                 n = (card c)

SystemF/SystemFImpl.hs

@@ -80,6 +80,7 @@ wellFormed (TyVar i) env             = case (nth env i) of
   Just Nil -> False
 wellFormed (TyArr ty1 ty2) env       = wellFormed ty1 env && wellFormed ty2 env
 wellFormed (TyAll ty) (ETypeVar env) = wellFormed ty env
+wellFormed (TyAll _)  _              = False
 wellFormed (TyBase) env              = True
 
 typeOf :: Term -> Env -> Either String Type