Commit 2949dab7 authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Partial working version of Comble-based System F term generator

Ability to generate terms based on types and to generate types of
arbitrary size. Missing the functionality to generate terms using type
applications (as this is very complex to write).
parent e28d12ec
......@@ -2,6 +2,7 @@ import Test.QuickCheck
import Control.Monad
import Control.Applicative
import qualified Data.Array as Arr
import qualified Data.Map as Map
import SystemFImpl
import HaskellOutput
......@@ -9,31 +10,41 @@ import Comble
data Abs = Term | Type
gentermoftype :: Alternative alt => Type -> Env -> Int -> alt Term
gentermoftype (TyBase) env 0 = asum [pure (TmNum n) | n <- [1..10]] -- Size zero constants: constants or variables
<|> asum (varsmatching TyBase env)
gentermoftype t env 0 = asum (varsmatching t env) -- Size zero for other types: a matching variable if one exists
gentermoftype (TyBase) env n = -- Constants
asum [TmApp <$> gentermoftype (TyArr t TyBase) env n1 <*> gentermoftype t env n2 | t <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching TyBase env)
<|> asum [pure (TmNum i) | i <- [1..10]]
gentermoftype (TyAll t) env n = -- Type abstraction
asum [TmApp <$> gentermoftype (TyArr t2 (TyAll t)) env n1 <*> gentermoftype t2 env n2 | t2 <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching (TyAll t) env)
<|> (TmTAbs <$> gentermoftype t (ETypeVar env) (n-1))
gentermoftype (TyArr l r) env n = -- Function types
asum [TmApp <$> gentermoftype (TyArr t (TyArr l r)) env n1 <*> gentermoftype t env n2 | t <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching (TyArr l r) env)
<|> (TmAbs <$> gentermoftype r (ETermVar l env) (n-1) <*> pure l)
gentermoftype (TyVar h) env n = -- Type variables
asum [TmApp <$> gentermoftype (TyArr t (TyVar h)) env n1 <*> gentermoftype t env n2 | t <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching (TyVar h) env)
varsmatching :: (Alternative alt) => Type -> Env -> [alt Term]
varsmatching a b = undefined
typesofsize :: Int -> [Type]
typesofsize n = undefined
termoftype :: Type -> Env -> Int -> Comble Term
termoftype _ _ 0 = empty
termoftype ty env 1 =
varsmatching ty env [] -- Size one: a matching variable if one exists
<|> case ty of (TyBase) -> pure $ TmNum 1 -- Or a constant if the type allows it
_ -> empty
termoftype ty env n =
asum [TmApp <$> termoftype (TyArr t ty) env n1 <*> termoftype t env n2 | t <- toList $ typeuptosize (n-1), (n1,n2) <- split2 (n-1)]
-- <|> asum [TmTApp <$> termoftype t1 env n <*> t2 | (t1, t2) <- splittypes ty]
<|> case ty of (TyBase) -> empty -- Constants
(TyAll t) -> TmTAbs <$> termoftype t (ETypeVar env) (n-1) -- Type abstraction
(TyArr l r) -> TmAbs <$> termoftype r (ETermVar l env) (n-1) <*> pure l -- Term abstraction
(TyVar h) -> empty -- Type variables
varsmatching :: Type -> Env -> [Abs] -> Comble Term
varsmatching _ Nil _ = empty
varsmatching ty (ETypeVar env) abs = varsmatching ty env (Type:abs)
varsmatching ty (ETermVar varty env) abs = (if (ty == varty)
then pure $ TmVar $ mkvar abs
else empty)
<|> varsmatching ty env (Term:abs)
typeofsize :: Int -> Int -> Comble Type
typeofsize 0 _ = empty
typeofsize 1 d = pure (TyBase)
<|> asum [pure $ TyVar $ mkvar $ take i $ repeat Type | i <- [0..(d-1)]]
typeofsize n d = asum [TyArr <$> typeofsize n1 d <*> typeofsize n2 d | (n1,n2) <- split2 (n-1)]
<|> (TyAll <$> typeofsize (n-1) (d+1))
typeuptosize :: Int -> Comble Type
typeuptosize 0 = empty
typeuptosize n = typeofsize n 0 <|> typeuptosize (n-1)
--subtypes :: Type -> [(Type,Type)]
mkvar :: [Abs] -> HNat
mkvar [] = Z
......
Supports Markdown
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