Commit 32ee3cca authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Merge branch 'master' of github.com:martonbognar/ASTTool into genterm

parents e2209fbd 55dd621b
asttool : *.hs
ghc Test.hs Comble.hs SystemFImpl.hs SystemFSorts.hs -dynamic -o test
ghc Test.hs Comble.hs SystemFImpl.hs SystemFBase.hs -dynamic -o test
clean :
rm test *.o *.hi
module SystemFBase where
import Data.List
import Control.Applicative
import Comble
......@@ -15,16 +16,15 @@ data Type = TyVar Variable | TyArr Type Type | TyAll Type | TyBase deriving(Show
plus (Z) h = h
plus h (Z) = h
plus x1 (STermVar x2) = (STermVar (plus x1 x2))
plus x1 (STypeVar x2) = (STypeVar (plus x1 x2))
plus x1 (STermVar x2) = (STermVar (plus x1 x2))
minus (Z) (Z) = (Z)
minus (Z) _ = (error "You cannot substract zero with a positive number")
minus result (Z) = result
minus (STermVar h1) (STermVar h2) = (minus h1 h2)
minus (STermVar h1) (STypeVar h2) = (error "differing namespace found in minus")
minus (STypeVar h1) (STermVar h2) = (error "differing namespace found in minus")
minus (STypeVar h1) (STypeVar h2) = (minus h1 h2)
minus (STermVar h1) (STermVar h2) = (minus h1 h2)
minus _ _ = (error "differing namespace found in minus")
generateHnatTermVar 0 c = c
generateHnatTermVar n c = (STermVar (generateHnatTermVar (n - 1) c))
......@@ -82,9 +82,9 @@ 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 (typeEnv env) nType))
<|> (asum (map (\l -> (TmApp <$> (termOfSize (termEnv env) ((!!) l 0) nType) <*> (termOfSize (termEnv env) ((!!) l 1) nType))) (splitn 2 (nTerm - 1))))
<|> (TmTApp <$> (termOfSize (termEnv env) (nTerm - 1) nType) <*> (typeUpToSize (typeEnv env) nType))
termOfSize env nTerm nType = ((TmAbs <$> (termOfSize (termEnv (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)))
termUpToSize env 0 nType = (empty)
......@@ -103,7 +103,7 @@ forTermWithSize env nTerm nType prop = (let c = (termOfSize env nTerm nType)
typeOfSize env 0 = (empty)
typeOfSize env 1 = ((TyVar <$> (getTypeVar env (Z)))
<|> (pure TyBase))
typeOfSize env nType = ((asum (map (\l -> (TyArr <$> (typeOfSize (typeEnv env) ((!!) l 0)) <*> (typeOfSize (typeEnv env) ((!!) l 1)))) (splitn 2 (nType - 1))))
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))))
typeUpToSize env 0 = (empty)
......@@ -136,13 +136,12 @@ getTypeVar (Z) _ = (empty)
getTypeVar (STypeVar next) abs = ((pure (reverseVar abs (Z)))
<|> (getTypeVar next (STypeVar abs)))
getTypeVar (STermVar next) abs = (getTypeVar next (STermVar abs))
instance Ord Variable where
compare (Z) (Z) = (EQ)
compare (Z) _ = (LT)
compare _ (Z) = (GT)
compare (STermVar h1) (STermVar h2) = (compare h1 h2)
compare (STermVar h1) (STypeVar h2) = (error "differing namespace found in compare")
compare (STypeVar h1) (STermVar h2) = (error "differing namespace found in compare")
compare (STypeVar h1) (STypeVar h2) = (compare h1 h2)
-- Custom, non-generated code
......@@ -182,13 +181,12 @@ 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 (typeEnv env) nType))
<|> (asum (map (\l -> (TmApp <$> (memo (termEnv env) ((!!) l 0)) <*> (memo (termEnv env) ((!!) l 1)))) (splitn 2 (nTerm - 1))))
<|> (TmTApp <$> (memo (termEnv env) (nTerm - 1)) <*> (typeUpToSize (typeEnv env) nType))
go env nTerm = ((TmAbs <$> (memo (termEnv (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))))
forMemoTermWithSize env nTerm nType prop = (let c = (memoTerm env nTerm nType)
n = (card c)
g = ((Comble.!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
in (forAll g prop))
module SystemFImpl (
Env(Nil, ETermVar, ETypeVar),
isVal,
getTypeFromEnv,
stepEval,
fullEval,
typeOf
) where
module SystemFImpl where
import SystemFBase
countTyped :: Either a b -> (Integer, Integer)
countTyped (Left l) = (1, 0)
countTyped (Right r) = (0, 1)
sumTuples (xl, xr) (yl, yr) = (xl + yl, xr + yr)
data Env
= Nil
| ETypeVar Env
| ETermVar Type
Env
deriving (Show, Eq)
data Env = ETermVar Type Env
| ETypeVar Env
| Nil
nth :: Env -> Variable -> Maybe Env
nth env Z = Just env
nth (ETypeVar env) (STypeVar x) = nth env x
nth (ETermVar _ env) (STermVar x) = nth env x
nth _ _ = Nothing
isVal :: Term -> Bool
isVal (TmAbs x t) = True
......@@ -28,9 +24,10 @@ getTypeFromEnv :: Env -> Variable -> Either String Type
getTypeFromEnv (ETermVar ty _) Z = return ty
getTypeFromEnv _ Z = Left "wrong or no binding for term"
getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (STermVar h) = Left "wrong term binding"
getTypeFromEnv (ETypeVar rest) (STypeVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (STermVar h) = Left "wrong term binding"
getTypeFromEnv _ (STypeVar h) = Left "No variable type"
--evaluation
stepEval :: Term -> Maybe Term
--function application
......@@ -66,12 +63,23 @@ fullEval t = maybe t (fullEval) t2
where
t2 = stepEval t
wellFormed :: Type -> Env -> Bool
wellFormed (TyVar i) env = case (nth env i) of
Nothing -> False
Just (ETermVar _ _) -> False
Just (ETypeVar _) -> True
Just Nil -> False
wellFormed (TyArr ty1 ty2) env = wellFormed ty1 env && wellFormed ty2 env
wellFormed (TyAll ty) env = wellFormed ty (ETypeVar env)
wellFormed (TyBase) env = True
typeOf :: Term -> Env -> Either String Type
typeOf (TmVar nat) ctx = getTypeFromEnv ctx nat
typeOf (TmAbs t ty) ctx = do
ty2 <- typeOf t (ETermVar ty ctx)
return (TyArr ty ty2)
typeOf (TmAbs t ty) ctx =
if (wellFormed ty ctx) then do
ty2 <- typeOf t (ETermVar ty ctx)
return (TyArr ty ty2)
else Left (show ty ++ " is not well-formed")
typeOf (TmApp t1 t2) ctx =
case (typeOf t1 ctx) of
Right (TyArr ty1 ty2) ->
......@@ -83,15 +91,13 @@ typeOf (TmApp t1 t2) ctx =
Left a -> Left a
Left a -> Left a
_ -> Left "arrow type expected"
typeOf (TmTApp t ty) ctx =
case (typeOf t ctx) of
Right (TyAll ty2) ->
return
(typeshiftminus
(STypeVar Z)
(typeTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
Left a -> Left a
_ -> Left "not a type abstraction"
typeOf (TmTApp (TmTAbs t) ty) ctx =
if (wellFormed ty ctx) then
typeOf
(termshiftminus
(STypeVar Z)
(termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t)) ctx
else Left (show ty ++ " is not well-formed")
typeOf (TmTAbs t) ctx = do
ty <- typeOf t (ETypeVar ctx)
return (TyAll ty)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment