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

Finish type application generation

The code now properly generates all possible substitutions that may be
made in any given type, including taking free variables into account.
parent ddf0c80a
......@@ -27,6 +27,7 @@ termoftype ty env nte nty =
(TyVar h) -> empty -- Type variables
where tydepth (ETypeVar e) = 1 + tydepth e
tydepth (ETermVar _ e) = tydepth e
tydepth Nil = 0
-- Check the environment for variables matching the given type
varsmatching :: Type -> Env -> [Abs] -> Comble Term
......@@ -57,14 +58,14 @@ propersubtypes ty = tys
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
then ([shiftfree d $ 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
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
else (shiftfree d $ TyAll t) : next
go (TyArr l r) d = (cur, h)
where (nextl, hl) = go l d
(nextr, hr) = go r d
......@@ -72,30 +73,42 @@ propersubtypes ty = tys
next = nextl ++ nextr
cur = if h > 0
then next
else TyArr l r : next
else (shiftfree d $ 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)
singlesubstitutions :: Type -> Type -> [Type]
singlesubstitutions ty sub = subs
where (subs, _) = go ty 0
go :: Type -> Int -> ([Type], Int) -- We use this to only consider proper subtypes for substitution
go (TyBase) d = (pluscur 0 d TyBase [TyBase] , 0)
go (TyVar h) d = if n >= d
then (pluscur 0 d (TyVar h) [TyVar h], 0)
else ([TyVar h] , n+1)
where n = counth h
go (TyAll a) d = (pluscur (h-1) d (TyAll a) $ TyAll <$> next , h-1)
where (next, h) = go a (d+1)
go (TyArr l r) d = (pluscur h d (TyArr l r) $ TyArr <$> nextl <*> nextr, h)
where (nextl, hl) = go l d
(nextr, hr) = go r d
h = max hl hr
pluscur :: Int -> Int -> Type -> [Type] -> [Type]
pluscur h d t ts = if h <= 0 && shiftfree d t == sub
then TyVar (mktype d) : ts
else ts
-- 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 <- singlesubstitutions (shiftup ty) (shiftup tosub),
subbed /= (shiftup ty)]
where shiftup = typeshiftplus (STypeVar Z)
shiftdown = typeshiftminus (STypeVar Z)
-- Type equality, taking in account free variables
--tyequals
where shiftup = typeshiftplus (STypeVar Z)
shiftdown = typeshiftminus (STypeVar Z)
-- Shift down free variables based on depth
shiftfree :: Int -> Type -> Type
shiftfree d t = typeshiftminus (iterate STypeVar Z !! d) t
-- Create a variable based on a list of abstractions
mkvar :: [Abs] -> HNat
......
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