Commit ddf0c80a authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Split out type size in genterm, add TmTApp to generation

- Allows specifying the size of types in gentermoftype separately
- gentermoftype can use type variables from the env when generating
arrow terms
- Add not-fully-functioning generation of TmTApp terms. It does
currently not handle free variables properly.
parent a5f1732e
......@@ -3,6 +3,7 @@ import Control.Monad
import Control.Applicative
import qualified Data.Array as Arr
import qualified Data.Map as Map
import qualified Data.List as List
import SystemFImpl
import HaskellOutput
......@@ -10,20 +11,24 @@ import Comble
data Abs = Term | Type
termoftype :: Type -> Env -> Int -> Comble Term
termoftype _ _ 0 = empty
termoftype ty env 1 =
-- Generate a term with a certain type and size
termoftype :: Type -> Env -> Int -> Int -> Comble Term
termoftype _ _ 0 nty = empty
termoftype ty env 1 nty =
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
termoftype ty env nte nty =
asum [TmApp <$> termoftype (TyArr t ty) env n1 nty <*> termoftype t env n2 nty | t <- toList $ typeuptosize nty $ tydepth env, (n1,n2) <- split2 (nte-1)]
<|> asum [TmTApp <$> termoftype subbed env (nte-1) nty <*> pure tosub | (tosub, subbed) <- allsubstitutions ty]
<|> case ty of (TyBase) -> empty -- Constants
(TyAll t) -> TmTAbs <$> termoftype t (ETypeVar env) (nte-1) nty -- Type abstraction
(TyArr l r) -> TmAbs <$> termoftype r (ETermVar l env) (nte-1) nty <*> pure l -- Term abstraction
(TyVar h) -> empty -- Type variables
where tydepth (ETypeVar e) = 1 + tydepth e
tydepth (ETermVar _ e) = tydepth e
-- Check the environment for variables matching the given type
varsmatching :: Type -> Env -> [Abs] -> Comble Term
varsmatching _ Nil _ = empty
varsmatching ty (ETypeVar env) abs = varsmatching ty env (Type:abs)
......@@ -32,22 +37,97 @@ varsmatching ty (ETermVar varty env) abs = (if (ty == varty)
else empty)
<|> varsmatching ty env (Term:abs)
-- Generate a type of a given size and with up to a given number of free variables
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)]]
<|> asum [pure $ TyVar $ mktype i | 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)
-- Generate all types up to a given size, with up to a given number of free variables
typeuptosize :: Int -> Int -> Comble Type
typeuptosize 0 _ = empty
typeuptosize n d = typeofsize n d <|> typeuptosize (n-1) d
--subtypes :: Type -> [(Type,Type)]
-- Get all subtypes without freeing bound variables
propersubtypes :: Type -> [Type]
propersubtypes ty = tys
where (tys, _) = go ty 0
go :: Type -> Int -> ([Type], Int)
go (TyBase) d = ([TyBase], 0)
go (TyVar h) d = if n >= d
then ([TyVar h], 0) -- Variable free in original type: allowed in subtype
else ([] , n + 1) -- Variable bound in original type: not allowed in subtype
where n = counth h
go (TyAll t) d = (cur, h-1) -- h-1 because TyAll may be the abstraction that binds some variables
where (next, h) = go t (d+1)
cur = if h-1 > 0
then next
else TyAll t : next
go (TyArr l r) d = (cur, h)
where (nextl, hl) = go l d
(nextr, hr) = go r d
h = max hl hr
next = nextl ++ nextr
cur = if h > 0
then next
else TyArr l r : next
-- Return all possible ways to substitute a the second type into the first type
singlesubstitutions :: Type -> Type -> Int -> [Type]
singlesubstitutions ty sub d = case ty of (TyAll t) -> pluscur $ TyAll <$> singlesubstitutions t sub (d+1)
(TyArr l r) -> pluscur $ TyArr <$> singlesubstitutions l sub d <*> singlesubstitutions r sub d
_ -> pluscur [ty]
where pluscur :: [Type] -> [Type]
pluscur f = (if (ty == sub)
then TyVar (mktype d) : f
else f)
-- Return all substitutions that produce a given type
allsubstitutions :: Type -> [(Type,Type)]
allsubstitutions ty = [(tosub, TyAll subbed)
| tosub <- (List.nub . propersubtypes) ty,
subbed <- singlesubstitutions (shiftup ty) (shiftup tosub) 0,
subbed /= (shiftup ty)]
where shiftup = typeshiftplus (STypeVar Z)
shiftdown = typeshiftminus (STypeVar Z)
-- Type equality, taking in account free variables
--tyequals
-- Create a variable based on a list of abstractions
mkvar :: [Abs] -> HNat
mkvar [] = Z
mkvar (Term:as) = STermVar (mkvar as)
mkvar (Type:as) = STypeVar (mkvar as)
-- Make a type variable of size i
mktype :: Int -> HNat
mktype i = mkvar $ take i $ repeat Type
-- Count the absolute size of a variable
counth :: HNat -> Int
counth Z = 0
counth (STypeVar h) = 1 + counth h
counth (STermVar h) = 1 + counth h
----
-- Debug
----
-- Substitute the first type into the second type
reconstruct :: Type -> Type -> Type
--reconstruct tosub (TyAll subbed) = typeshiftminus (STypeVar Z) (typetypeSubstitute (typeshiftplus (STypeVar Z) tosub) Z subbed)
reconstruct tosub subbed = hackyextract $ typeOf (TmTApp (TmVar Z) tosub) (ETermVar subbed Nil)
-- Will crash if something goes wrong, but that's fine.
hackyextract :: Either String Type -> Type
hackyextract (Right t) = t
hackyextract (Left s) = undefined
-- Test whether the allsubstitutions function only produces correct substitutions
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]
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