Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
Checking mergeability… Don't worry, you can still create the pull request.
  • 2 commits
  • 11 files changed
  • 0 commit comments
  • 1 contributor
Commits on Sep 14, 2006
@amiddelk amiddelk Created a separate branch for a special version of my uniqueness
type system. It uses some recent ideas from my master's thesis
(like the beta-annotations).
ad79d0a
@amiddelk amiddelk Comitted a version of my uniqueness typing implementation that
is suitable for the Efficient Implementation of Functional
Languages course. It is a LOT easier (both in terms of implementation
as in terms of using the results) than my implementation
in the main uniqueness branch.

Unfortunately, this version is EH 2 only (whereas the implementation
in the main branch is EH 7/8). However, probably some special backend
is needed to exploit uniqueness information, so EH 2 might not be that
bad after all.
f1915d8
View
6 EHC/mk/shared.mk.in
@@ -118,8 +118,8 @@ GEN_CABAL = \
echo "Author: Atze Dijkstra" ; \
echo "Homepage: http://www.cs.uu.nl/wiki/Ehc/WebHome" ; \
echo "Category: Testing" ; \
- echo "Build-Depends: $(subst $(space),$(comma),$(strip base haskell98 uulib $(3)))" ; \
- echo "Extensions: $(subst $(space),$(comma),$(strip RankNTypes MultiParamTypeClasses FunctionalDependencies $(4)))" ; \
+ echo "Build-Depends: $(subst $(space),$(comma),$(strip base mtl fgl haskell98 uulib $(3)))" ; \
+ echo "Extensions: $(subst $(space),$(comma),$(strip RankNTypes MultiParamTypeClasses FunctionalDependencies UndecidableInstances))" ; \
echo "Synopsis: $(strip $(5))" ; \
echo "Exposed-Modules: $(subst $(space),$(comma),$(strip $(6)))" \
)
@@ -134,4 +134,4 @@ GHC_CABAL = $(GHC) -package Cabal -o $(2) $(1) ; $(STRIP_CMD) $(2)
# subst _ by x
# $1: text
-SUBS_US_X = $(subst _,x,$(1))
+SUBS_US_X = $(subst _,x,$(1))
View
130 EHC/src/ehc/EH/Infer.cag
@@ -187,7 +187,7 @@ ATTR AllDecl AllExpr [ valGam: ValGam | | ]
%%[1.initValGam
SEM AGItf
- | AGItf expr . valGam = emptyGam
+ | AGItf expr . valGam = gamFromAssocL [(HNm "plus", ValGamInfo { vgiTy = @loc.plusTy})]
%%]
%%[12 -1.initValGam
@@ -198,6 +198,133 @@ ATTR AGItf [ valGam: ValGam | | ]
ATTR AllDecl [ | patValGam: ValGam | ]
%%]
+%%[2
+ATTR AllDecl AllExpr [ bndgGam: ValGam ||]
+ATTR AllDecl AllExpr [ annGam: ValGam ||]
+ATTR AllDecl AllPatExpr [|| annGamCol USE {`gamAddGam`} {emptyGam}: ValGam ]
+
+SEM AGItf
+ | AGItf expr.bndgGam = trace ("initial: " ++ show @loc.initialBndgId)
+ $ gamFromAssocL [(HNm "plus", ValGamInfo { vgiTy = Ty_Var @loc.initialBndgId })]
+ expr.annGam = gamFromAssocL [(HNm "plus", ValGamInfo { vgiTy = @loc.plusAnnTy })]
+ loc.plusTy = Ty_App (Ty_App (Ty_Con hsnArrow [Ty_Var @loc.beta1]) (Ty_Con hsnInt [])) @loc.plusAux
+ loc.plusAux = Ty_App (Ty_App (Ty_Con hsnArrow [Ty_Var @loc.beta2]) (Ty_Con hsnInt [])) (Ty_Con hsnInt [])
+ loc.plusAnnTy = Ty_App (Ty_App (Ty_Ann @loc.delta1 (Ty_Con hsnArrow [Ty_Var @loc.beta1])) (Ty_Ann @loc.delta2 (Ty_Con hsnInt []))) @loc.plusAnnAux
+ loc.plusAnnAux = Ty_App (Ty_App (Ty_Ann @loc.delta3 (Ty_Con hsnArrow [Ty_Var @loc.beta2])) (Ty_Ann @loc.delta4 (Ty_Con hsnInt []))) (Ty_Ann @loc.delta5 (Ty_Con hsnInt []))
+
+
+ATTR AllDecl [|| bndgGamCol USE {`gamAddGam`} {emptyGam}: ValGam ]
+
+ATTR AllPatExpr [| valGam2 : ValGam |]
+SEM Expr
+ | Lam arg.valGam2 = emptyGam
+SEM PatExpr
+ | Var lhs.valGam2 = gamAdd @nm undefined @lhs.valGam2
+SEM Decl
+ | Val patExpr.valGam2 = emptyGam
+
+
+ATTR AllDecl AllExpr [|| bndgs USE {`mergeBndgs`} {emptyBndgs}: Bndgs uses USE {++} {[]}: {[(HsName,Ty)]} cs USE {++} {[]}: {[Constr]} ]
+ATTR AllPatExpr AllDecl [|| defs USE {++} {[]}: {[(HsName,Ty)]} ]
+ATTR AllExpr [|| annTy : Ty ]
+
+ATTR AllPatExpr [ annTyIn : Ty ||]
+SEM PatExpr
+ | App (func.annTyIn, arg.annTyIn) = let (Ty_App f a) = @lhs.annTyIn
+ in (f, a)
+ | Var lhs.defs = [(@nm, @lhs.annTyIn)]
+ lhs.annGamCol = gamUnit @nm (ValGamInfo { vgiTy = @lhs.annTyIn })
+SEM Expr
+ | Lam arg.annTyIn = @loc.ty_p_in_
+ (loc.sumCs, lhs.uses) = tyGathSums @arg.defs @body.uses
+ loc.annGam = @arg.annGamCol `gamAddGam` @lhs.annGam
+ | Let (loc.sumCs, loc.declUses) = tyGathSums @decls.defs (@decls.uses ++ @body.uses)
+ loc.annGam = @decls.annGamCol `gamAddGam` @lhs.annGam
+ lhs.uses = @body.uses ++ @loc.declUses
+ | Con lhs.uses = [(@nm, @loc.annTy_)]
+ | Var lhs.uses = [(@nm, @loc.annTy_)]
+SEM Decl
+ | Val patExpr.annTyIn = @loc.annTy_fresh_
+
+SEM Expr
+ | Var loc.defBndgTyId = maybe undefined vgiTy (@nm `gamLookup` @lhs.bndgGam )
+ loc.defBndgId = tyVarId (@lhs.finTyCnstr |=> @loc.defBndgTyId)
+ loc.defAnnTy = maybe undefined vgiTy (@nm `gamLookup` @lhs.annGam)
+ loc.pairs = [ let (Ty_Var a) = @lhs.finTyCnstr |=> ta
+ (Ty_Var b) = @lhs.finTyCnstr |=> tb
+ in (a, b)
+ | (ta,tb) <- @loc.pairs_ ]
+ loc.cs = [tyInst @loc.pairs @loc.defBndgId @loc.defAnnTy @loc.annTy_]
+ | Con loc.cs = []
+ | App (loc.annTy, loc.paramTy, loc.finBndgId, loc.spineAnn) = let (Ty_App (Ty_App (Ty_Ann a (Ty_Con _ [Ty_Var b])) p) r) = @func.annTy in (r, p, b, a)
+ loc.csParamArg = tyToCoercions @loc.paramTy @arg.annTy
+ loc.csFunSpine = [tyOutermostAnn @loc.annTy :=>=: @loc.spineAnn]
+ loc.argInst = [tyInst [] @loc.finBndgId @arg.annTy @paramTy]
+ loc.argBndg = singletonBndgs @loc.finBndgId [@arg.annTy] @arg.cs
+ loc.cs = @loc.csParamArg ++ @loc.csFunSpine ++ @loc.argInst ++ @func.cs
+ loc.bndgs = @loc.argBndg `mergeBndgs` @func.bndgs `mergeBndgs` @arg.bndgs
+ | Lam loc.cs = @loc.sumCs ++ @arg.cs ++ @body.cs
+ | Let loc.cs = @loc.sumCs ++ @decls.cs ++ @body.cs
+
+SEM Decl
+ | Val loc.resCs = tyToCoercions @loc.annTy_fresh_ @expr.annTy
+ loc.valCs = @loc.resCs ++ @expr.cs
+ loc.bndg = singletonBndgs @loc.bndgId_ [] @loc.valCs
+ lhs.bndgs = @loc.bndg `mergeBndgs` @expr.bndgs
+ lhs.cs = @patExpr.cs
+
+ATTR AllExpr AllPatExpr AllDecl [ enclosingAnn : UID ||]
+ATTR AllPatExpr [|| cs USE {++} {[]} : {[Constr]} ]
+
+SEM AGItf
+ | AGItf expr.enclosingAnn = error "Enclosing ann of root of the AST used"
+
+SEM Expr
+ | Let loc.enclosingAnn = tyOutermostAnn @body.annTy
+ | Lam loc.enclosingAnn = tyOutermostAnn @loc.annTy
+
+SEM PatExpr
+ | Con loc.cs = [@lhs.enclosingAnn :=>=: tyOutermostAnn @lhs.annTyIn]
+
+SEM AGItf
+ | AGItf (loc.lUniq2, loc.initialBndgId, loc.rootBndgId, loc.deltaRoot) = mkNewLevUID3 @loc.lUniq
+ loc.cs = [[@loc.deltaRoot] :<=: tyOutermostAnn @expr.annTy] ++ @expr.cs
+ loc.initialCs = [@loc.delta5 :=>=: @loc.delta3, @loc.delta5 :=>=: @loc.delta4]
+ loc.bndg = singletonBndgs @loc.rootBndgId [] @loc.cs `mergeBndgs` singletonBndgs @loc.initialBndgId [] @loc.initialCs
+ loc.bndgs = @loc.bndg `mergeBndgs` @expr.bndgs
+
+ (loc.lUniq3, loc.delta1, loc.delta2, loc.delta3, loc.delta4) = mkNewLevUID4 @loc.lUniq2
+ (loc.lUniq4, loc.delta5, loc.beta1, loc.beta2) = mkNewLevUID3 @loc.lUniq3
+
+ATTR AllDecl AllExpr AllPatExpr [|| sacredAnns USE {++} {[]} : {[(HsName, UID)]} ]
+SEM Expr
+ | Lam lhs.sacredAnns = filter (\(n,_) -> not (n `elem` (map fst @arg.sacredAnns))) @body.sacredAnns
+ | Var lhs.sacredAnns = map (\x -> (@nm, x)) (tyAnns @loc.annTy)
+ | Con lhs.sacredAnns = map (\x -> (@nm, x)) (tyAnns @loc.annTy)
+ | Let lhs.sacredAnns = filter (\(n,_) -> not (n `elem` (map fst @decls.sacredAnns))) @body.sacredAnns
+SEM PatExpr
+ | Var lhs.sacredAnns = map (\x -> (@nm, x)) (tyAnns @lhs.annTyIn)
+
+ATTR AllDecl AllExpr [ sacredAnnsIn : {[UID]} ||]
+SEM AGItf
+ | AGItf expr.sacredAnnsIn = map snd @expr.sacredAnns
+SEM Expr
+ | Lam body.sacredAnnsIn = @lhs.sacredAnnsIn ++ map snd @arg.sacredAnns
+ | Let loc.sacredAnnsIn = @lhs.sacredAnnsIn ++ map snd @decls.sacredAnns
+
+ATTR AllDecl AllExpr [|| sacredAnnsOut USE {++} {[]} : {[(UID,[UID])]}]
+SEM Expr
+ | App lhs.sacredAnnsOut = [(@loc.finBndgId, @lhs.sacredAnnsIn)] ++ @func.sacredAnnsOut ++ @arg.sacredAnnsOut
+SEM Decl
+ | Val lhs.sacredAnnsOut = [(@loc.bndgId_, @lhs.sacredAnnsIn)] ++ @expr.sacredAnnsOut
+
+SEM AGItf
+ | AGItf loc.sacsForSolver = trace ("initial bndg id: " ++ show @loc.initialBndgId ++", root bndg id: " ++ show @loc.rootBndgId ++ "\n" ++ show @loc.bndgs)
+ $ mkSacsMap ([(@loc.initialBndgId, []), (@loc.rootBndgId, map snd @expr.sacredAnns)]++ @expr.sacredAnnsOut)
+ loc.res = solve @loc.bndgs @loc.sacsForSolver @loc.rootBndgId @loc.deltaRoot
+
+%%]
+
-- generated from ruler rules into EHRulerRules, was 1.patValGam.Val
%%[5.patValGam.Val
SEM Decl
@@ -749,4 +876,3 @@ SEM Expr
body . prIntroGam = gamPushGam @lQuPrIGam @gSubsPrIGam
%%]
-
View
2  EHC/src/ehc/EH/MainAG.cag
@@ -10,7 +10,7 @@
%%[1 hs module {%{EH}EH.MainAG} import(Data.Char,Data.List as List,EH.Util.Utils,UU.Pretty, EH.Util.PPUtils,{%{EH}Base.Common},{%{EH}Base.Opts}, {%{EH}Ty},{%{EH}Gam},{%{EH}Error},{%{EH}Error.Pretty},{%{EH}Ty.FitsIn},{%{EH}Ty.FitsInCommon},{%{EH}Ty.Pretty},{%{EH}EH})
%%]
-%%[2 hs import({%{EH}Cnstr},{%{EH}Substitutable},Data.Maybe)
+%%[2 hs import({%{EH}Cnstr},{%{EH}Substitutable},Data.Maybe,qualified Data.Map as Map, Data.Map(Map),Debug.Trace)
%%]
%%[3 hs import({%{EH}Ty.Quantify},{%{EH}Ty.Instantiate})
View
6 EHC/src/ehc/EH/Pretty.cag
@@ -13,7 +13,7 @@ ATTR AllNT AGItf [ | | pp USE {>-<} {empty} : PP_Doc ]
SEM Expr
| IConst loc . pp = pp (show @int)
| CConst loc . pp = pp (show @char)
- | Var loc . pp = pp @nm
+ | Var loc . pp = "(" >|< pp @nm >#< "::" >#< ppTy @loc.annTy_ >|< " | " >|< show @loc.cs >|< ")"
| Con loc . pp = ppCon @nm
| Let loc . pp = "let"
>#< (@decls.pp >-< @ppExtra)
@@ -40,7 +40,7 @@ SEM Decl
SEM PatExpr
| IConst loc . pp = pp (show @int)
| CConst loc . pp = pp (show @char)
- | Var loc . pp = pp @nm
+ | Var loc . pp = "(" >|< pp @nm >#< "::" >#< ppTy @lhs.annTyIn >|< ")"
| VarAs loc . pp = pp @nm >|< "@" >|< @patExpr.pp
| Con loc . pp = ppCon @nm
| App loc . pp = @func.pp >#< @arg.pp
@@ -59,7 +59,7 @@ SEM Decls
| Cons lhs . pp = @hd.pp >-< @errPP >-< @tl.pp
SEM AGItf
- | AGItf lhs . pp = @ppExtra >-< @expr.pp >-< @errTopPP
+ | AGItf lhs . pp = @ppExtra >-< @expr.pp >-< @errTopPP >-< " " >-< "bndgs: " >-< (" " >|< (foldr (>-<) empty [pp b >|< ": " >|< show cs | (b, cs) <- Map.toList @loc.bndgs])) >-< " " >-< "sol:" >-< (" " >|< show @loc.res)
loc . ppExtra = empty
%%]
View
4 EHC/src/ehc/EH/Uniq.cag
@@ -26,10 +26,10 @@ SEM PatExpr
| Var (lhs.gUniq,loc.lUniq) = mkNewLevUID @lhs.gUniq
| VarAs (patExpr.gUniq,loc.lUniq) = mkNewLevUID @lhs.gUniq
| Con (lhs.gUniq,loc.lUniq) = mkNewLevUID @lhs.gUniq
-
+
%%[2
SEM AGItf
- | AGItf expr . gUniq = uidStart
+ | AGItf (expr.gUniq, loc.lUniq) = mkNewLevUID uidStart
%%]
-- generated from ruler rules into EHRulerRules
View
15 EHC/src/ehc/Gam.chs
@@ -31,6 +31,9 @@
%%[2 import({%{EH}Cnstr},{%{EH}Substitutable})
%%]
+%%[2 export(valGamToBndgGam)
+%%]
+
%%[3 import({%{EH}Ty.Quantify}) export(valGamQuantify,gamMapElts,valGamMapTy)
%%]
@@ -123,7 +126,7 @@ gamAdd k v g = gamAddGam (k `gamUnit` v) g
%%]
%%[9.Base.funs -1.Base.funs
-emptyGam = emptyTGam 1
+emptyGam = emptyTGam 1
gamUnit = tgamUnit 1
gamLookup k g = tgamLookup (tgamSize1 g) k g
gamToAssocL g = tgamToAssocL (tgamSize1 g) g
@@ -604,7 +607,7 @@ data TyGamInfo = TyGamInfo { tgiTy :: Ty } deriving Show
tyGamLookup :: HsName -> TyGam -> Maybe TyGamInfo
tyGamLookup nm g
= case gamLookup nm g of
- Nothing | hsnIsProd nm -> Just (TyGamInfo (Ty_Con nm))
+-- Nothing | hsnIsProd nm -> Just (TyGamInfo (Ty_Con nm))
Just tgi -> Just tgi
_ -> Nothing
%%]
@@ -860,7 +863,7 @@ instance PP TyGamInfo where
initTyGam :: TyGam
initTyGam
= assocLToGam
- [ (hsnArrow, TyGamInfo (Ty_Con hsnArrow))
+ [ (hsnArrow, TyGamInfo (Ty_Con hsnArrow (error "Uninstantiated bndg id")))
, (hsnInt, TyGamInfo tyInt)
, (hsnChar, TyGamInfo tyChar)
]
@@ -904,3 +907,9 @@ initKiGam
]
%%]
+%%[2
+valGamToBndgGam :: UID -> ValGam -> ValGam
+valGamToBndgGam bndgId valGam
+ = assocLToGam [ (x, ValGamInfo { vgiTy = Ty_Var bndgId }) | (x, _) <- gamToAssocL valGam ]
+%%]
+
View
286 EHC/src/ehc/Ty.cag
@@ -10,10 +10,13 @@
%%[1 hs module {%{EH}Ty} import(EH.Util.Utils,{%{EH}Base.Common}) export(TyAGItf(..), Ty(..), TyL, tyInt, tyChar, mkTyCon)
%%]
-%%[1 hs export(tyLHdAndTl, tyArrowArgRes, tyArrowArgsRes, tyArrowArgs, tyArrowRes, tyAppFunArgs, tyProdArgs, tyAppArgs)
+%%[1 hs export(tyLHdAndTl, tyArrowArgRes, tyArrowArgsRes, tyArrowArgs, tyArrowRes, tyAppFunArgs, tyProdArgs, tyAppArgs,BndgIdList)
%%]
-%%[2 hs export(TyVarId, TyVarIdL, mkTyVar, mkNewTyVar, mkNewUIDTyVarL, mkNewTyVarL, mkTyFreshProd, mkTyFreshProdFrom, tyEnsureNonAny)
+%%[2 hs import(Data.Map(Map), qualified Data.Map as Map, Data.List(intersect, partition, nub), Data.Maybe, Debug.Trace)
+%%]
+
+%%[2 hs export(TyVarId, TyVarIdL, mkTyVar, mkNewTyVar, mkNewUIDTyVarL, mkNewTyVarL, mkTyFreshProd, mkTyFreshProdFrom, tyEnsureNonAny, mkBndgArr, tyExtractBndgs, tyAnnotate, tyOutermostAnn, tyToCoercions, tyGathSums, Constr(..), tyInst, mergeBndgs, singletonBndgs, emptyBndgs, Bndgs, tyVarId, mkBndgAnnArr, bndgIdInst, worklistFix, SolveConstr(..), flatten, solve, tyAnns, mkSacsMap)
%%]
%%[3 hs export(mkTyQu, TyVarCateg(..))
@@ -22,7 +25,7 @@
%%[3 hs import(Data.Maybe) export(tyVar)
%%]
-%%[4 hs export(TyQu(..), tyquExists, tyquIsExists, tyquIsForall, showTyQu)
+%%[4 hs export(TyQu(..), tyquExists, tyquIsExists, tyquIsForall, showTyQu)
%%]
%%[4 hs export(tyConNm)
@@ -31,37 +34,37 @@
%%[4 hs export(tvCatIsFixed)
%%]
-%%[4 hs import(qualified Data.Map as Map) export(TvCatMp)
+%%[4 hs import(qualified Data.Map as Map) export(TvCatMp)
%%]
-%%[4_2 hs export(tyMbQu,tyIsQu,tyIsVar,tyMbVar,tyIsAlts)
+%%[4_2 hs export(tyMbQu,tyIsQu,tyIsVar,tyMbVar,tyIsAlts)
%%]
-%%[4_2 hs export(TyPlus(..),TyPlusL,tyPlusTy)
+%%[4_2 hs export(TyPlus(..),TyPlusL,tyPlusTy)
%%]
-%%[4_2 hs export(TyHardness(..))
+%%[4_2 hs export(TyHardness(..))
%%]
-%%[4_2 hs export(TyNeed(..))
+%%[4_2 hs export(TyNeed(..))
%%]
-%%[5 hs export(tyString)
+%%[5 hs export(tyString)
%%]
-%%[6 hs export(kiStar)
+%%[6 hs export(kiStar)
%%]
-%%[6_4 hs export(tvIsEx)
+%%[6_4 hs export(tvIsEx)
%%]
-%%[7 hs import(Data.List) export(rowExtCmp,rowLabCmp,tyRowCanonOrder,kiRow,tyRowEmpty,tyRecEmpty,tySumEmpty,tyRowExtr,tyRecExtr,mkTyRow,mkTyRec,mkTySum,mkTyRecExt,tyRowExts)
+%%[7 hs import(Data.List) export(rowExtCmp,rowLabCmp,tyRowCanonOrder,kiRow,tyRowEmpty,tyRecEmpty,tySumEmpty,tyRowExtr,tyRecExtr,mkTyRow,mkTyRec,mkTySum,mkTyRecExt,tyRowExts)
%%]
%%[7 hs export(tyAppFunArg)
%%]
-%%[8 hs export(tyFloat)
+%%[8 hs export(tyFloat)
%%]
%%[8 hs export(tyAppFunConNm)
@@ -94,7 +97,7 @@
%%[10 hs export(tyExtsOffset)
%%]
-%%[99 hs export(tyInteger,tyDouble)
+%%[99 hs export(tyInteger,tyDouble)
%%]
%%[1 import({Ty/AbsSyn})
@@ -286,9 +289,9 @@ tyIsQu = isJust . tyMbQu
instance SemApp Ty where
semApp = Ty_App
semAppTop = id
- semCon = Ty_Con . mkHNm
+ semCon = (\nm -> Ty_Con nm (error "Need bndgs: tysigs not allowed for uniqueness inference.")) . mkHNm
semParens = id
- mkRngCon _ = Ty_Con . mkHNm
+ mkRngCon _ = (\nm -> Ty_Con nm (error "Need bndgs: tysigs not allowed for uniqueness inference.")) . mkHNm
%%]
%%[1.mkRngVar hs
mkRngVar = mkRngCon
@@ -305,6 +308,14 @@ mkTyCon :: String -> Ty
mkTyCon n = semCon (HNm n)
%%]
+%%[2 hs
+mkBndgArr :: TyVarId -> Ty -> Ty -> Ty
+mkBndgArr u a r = Ty_App (Ty_App (Ty_Con hsnArrow [mkTyVar u]) a) r
+
+mkBndgAnnArr :: UID -> TyVarId -> Ty -> Ty -> Ty
+mkBndgAnnArr u1 u2 a r = Ty_App (Ty_App (Ty_Ann u1 (Ty_Con hsnArrow [mkTyVar u2])) a) r
+%%]
+
%%[2.mkTyVar hs
mkTyVar :: TyVarId -> Ty
mkTyVar tv = Ty_Var tv
@@ -390,11 +401,11 @@ mkTyPr p
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%[1.tyInt hs
-tyInt = Ty_Con hsnInt
+tyInt = Ty_Con hsnInt []
%%]
%%[1.tyChar hs
-tyChar = Ty_Con hsnChar
+tyChar = Ty_Con hsnChar []
%%]
%%[5.tyString hs
@@ -448,7 +459,7 @@ tyLHdAndTl :: [Ty] -> (Ty,TyL)
%%[1.unMkTy.tyArrowArgRes hs
tyArrowArgRes t
= case t of
- Ty_App (Ty_App (Ty_Con nm) a) r
+ Ty_App (Ty_App (Ty_Con nm _) a) r
| hsnIsArrow nm -> (a,r)
_ -> (Ty_Any,t)
%%]
@@ -456,16 +467,29 @@ tyArrowArgRes t
%%[1.unMkTy.tyArrowArgsRes hs
tyArrowArgsRes t
= case t of
- Ty_App (Ty_App (Ty_Con nm) a) r
+ Ty_App (Ty_App (Ty_Con nm _) a) r
| hsnIsArrow nm -> let (as,r') = tyArrowArgsRes r in (a:as,r')
_ -> ([],t)
%%]
+%%[2 hs
+tyExtractBndgs :: Ty -> [TyVarId]
+tyExtractBndgs ty
+ = case ty of
+ Ty_App f _ -> tyExtractBndgs f
+ Ty_Var _ -> []
+ Ty_Con _ bndgs -> [b | Ty_Var b <- bndgs]
+
+tyVarId :: Ty -> TyVarId
+tyVarId (Ty_Var v) = v
+tyVarId _ = error "tyVarId: no Ty_Var"
+%%]
+
%%[8.unMkTy.tyArrowArgsRes -1.unMkTy.tyArrowArgsRes hs
tyArrowArgsRes t
= case t of
Ty_Quant _ _ t -> tyArrowArgsRes t
- Ty_App (Ty_App (Ty_Con nm) a) r
+ Ty_App (Ty_App (Ty_Con nm _) a) r
| hsnIsArrow nm -> let (as,r') = tyArrowArgsRes r in (a:as,r')
_ -> ([],t)
%%]
@@ -748,3 +772,223 @@ implsPrIds = map poPoi . fst . implsPredsTail
data TyCtxt = TyCtxt_Ty | TyCtxt_Pred | TyCtxt_Class deriving (Show,Eq)
%%]
+
+%%[2 hs
+mergeBndgs :: Bndgs -> Bndgs -> Bndgs
+mergeBndgs = Map.unionWith (\(a,b) (c,d) -> (a++c,b++d))
+
+singletonBndgs :: UID -> [Ty] -> [Constr] -> Bndgs
+singletonBndgs u tps cs = Map.singleton u (tps, cs)
+
+emptyBndgs :: Bndgs
+emptyBndgs = Map.empty
+
+tyAnnotate :: Ty -> UID -> (Ty, UID)
+tyAnnotate t u
+ = case t of
+ Ty_App f a -> let (f1, u1) = tyAnnotate f u
+ (a1, u2) = tyAnnotate a u1
+ in (Ty_App f1 a1, u2)
+ t1@(Ty_Var _) -> let (u2, u1) = mkNewUID u
+ in (Ty_Ann u1 t1, u2)
+ t1@(Ty_Con _ _) -> let (u2, u1) = mkNewUID u
+ in (Ty_Ann u1 t1, u2)
+
+tyOutermostAnn :: Ty -> UID
+tyOutermostAnn t
+ = case t of
+ Ty_App f _ -> tyOutermostAnn f
+ Ty_Ann u _ -> u
+ _ -> error "tyOutermostAnn: no such outermost ann"
+
+tyAnns :: Ty -> [UID]
+tyAnns t
+ = case t of
+ Ty_App f a -> tyAnns f ++ tyAnns a
+ Ty_Ann u _ -> [u]
+
+tyToCoercions :: Ty -> Ty -> [Constr]
+tyToCoercions (Ty_App (Ty_App (Ty_Ann u1 (Ty_Con nm1 _)) a1) b1) (Ty_App (Ty_App (Ty_Ann u2 (Ty_Con nm2 _)) a2) b2)
+ | nm1 == hsnArrow
+ = [ u1 :=>=: u2 ]
+ ++ tyToCoercions a2 a1
+ ++ tyToCoercions b1 b2
+tyToCoercions (Ty_App f1 a1) (Ty_App f2 a2)
+ = tyToCoercions f1 f2
+ ++ tyToCoercions a1 a2
+tyToCoercions (Ty_Ann u1 _) (Ty_Ann u2 _)
+ = [ u1 :=>=: u2 ]
+
+tyGathSums :: [(HsName, Ty)] -> [(HsName, Ty)] -> ([Constr], [(HsName, Ty)])
+tyGathSums pats gats
+ = ( [ [tyOutermostAnn t | (n,t) <- gats, n == nm] :<=: tyOutermostAnn ty | (nm, ty) <- pats ]
+ , filter (not . (`elem` (map fst pats)) . fst) gats
+ )
+
+tyInst :: [(UID,UID)] -> UID -> Ty -> Ty -> Constr
+tyInst pairs bndgId tyA tyB
+ = Inst pairs bndgId tyA tyB
+
+eqs' tyL ty = concatMap (\t -> eqs t ty) tyL
+eqs (Ty_App f1 a1) (Ty_App f2 a2)
+ = eqs f1 f2 ++ eqs a1 a2
+eqs (Ty_Ann u1 _) (Ty_Ann u2 _)
+ = [(u1,u2)] --[(u1,u2),(u2,u1)]
+eqs _ _
+ = error "tyInst: tycon encountered: type not annotated?"
+
+bndgIdInst :: UID -> Ty -> (Ty, [(Ty, Ty)])
+bndgIdInst uid ty
+ = let (t, pairs, _) = rec uid ty in (t, pairs)
+ where
+ rec uid ty
+ = case ty of
+ Ty_App f a -> let (f1, fp, uid1) = rec uid f
+ (a1, ap, uid2) = rec uid1 a
+ in (f1 `Ty_App` a1, fp ++ ap, uid2)
+ Ty_Ann u t -> let (t', p, uid') = rec uid t
+ in (Ty_Ann u t', p, uid')
+ Ty_Con nm bndgIds -> let (uid1, uid2) = mkNewLevUID uid
+ uidL = mkInfNewUIDL uid2
+ bndgIds' = map (Ty_Var) (take (length bndgIds) uidL)
+ p = zip bndgIds bndgIds'
+ in (Ty_Con nm bndgIds', p, uid1)
+ t@(Ty_Var _) -> (t, [], uid)
+
+%%]
+
+%%[2 hs
+data Constr
+ = UID :=>=: UID
+ | [UID] :<=: UID
+ | Inst [(UID, UID)] UID Ty Ty
+ deriving (Eq, Ord, Show)
+
+data SolveConstr a
+ = a ::=>=:: a
+ | [a] ::<=:: a
+ deriving (Eq, Ord, Show)
+
+type Bndgs = Map UID ([Ty], [Constr])
+
+worklistFix :: Eq a => (SolveConstr a -> SolveConstr a) -> a -> [SolveConstr UID] -> Map UID a -> Map UID a
+worklistFix solveF bot cs initial
+ = iter cs initial
+ where
+ deps = [ (c, [d | d <- cs, c `shareVar` d, c /= d]) | c <- cs ]
+
+ shareVar p q = shareVarAux2 (shareVarAux1 p) (shareVarAux1 q)
+ shareVarAux1 (a ::=>=:: b) = [a, b]
+ shareVarAux1 (al ::<=:: b) = b: al
+ shareVarAux2 p q = not (null (intersect p q))
+
+ iter [] subst = subst
+ iter (c : cs) subst
+ = let c1 = subst `apply` c
+ c2 = solveF c1
+ subst' = (c, c2) `update` subst
+ in if subst' == subst
+ then iter cs subst'
+ else iter ((c `lookup'` deps) ++ cs) subst'
+
+ apply s (a ::=>=:: b)
+ = applyAux s a ::=>=:: applyAux s b
+ apply s (al ::<=:: b)
+ = map (applyAux s) al ::<=:: applyAux s b
+ applyAux
+ = flip (Map.findWithDefault bot)
+
+ update (ua ::=>=:: ub, a ::=>=:: b) s
+ = updateAux ub b (updateAux ua a s)
+ update (ual ::<=:: ub, al ::<=:: b) s
+ = foldr (uncurry updateAux) (updateAux ub b s) (zip ual al)
+ updateAux
+ = Map.insert
+
+ lookup' k h = maybe [] id (lookup k h)
+
+upperSolveF (a ::=>=:: b)
+ = a ::=>=:: ((a `max` b) `min` 2)
+upperSolveF (l ::<=:: b)
+ = let z = sum l
+ in l ::<=:: ((b `max` z) `min` 2)
+
+flatten :: Bndgs -> UID -> Map UID [UID] -> [SolveConstr UID]
+flatten bndgs outermostId sacreds
+ = fst $ construct outermostId [] (uidChild outermostId)
+ where
+ construct bndgId idMap uid
+ = let -- cs = Map.findWithDefault (error ("cannot find cs: " ++ show bndgId ++ " | " ++ show bndgs)) bndgId bndgs
+ (mCanonTy, cs) = Map.findWithDefault ( trace ("no cs info for: " ++ show bndgId) ([], [])) bndgId bndgs
+ cs' = rename cs idMap
+ (csI, csN) = partition isInst cs'
+ csN' = map toSolveConstr csN
+ csN'' = foldr (uncurry (instantiate bndgId)) csN' (zip (mkInfNewUIDL uid) csI)
+ in (csN'', mCanonTy)
+
+ toSolveConstr (a :=>=: b) = a ::=>=:: b
+ toSolveConstr (a :<=: b) = a ::<=:: b
+
+ rename cs idMap
+ = map ren cs
+ where
+ ren (Inst mp bndgId fromTy toTy) = Inst [(renAux a, renAux b) | (a,b) <- mp ] (renAux bndgId) fromTy toTy
+ ren c = c
+ renAux a = maybe a id (a `lookup` idMap)
+
+ insts cs = [c | c <- cs, isInst c]
+ isInst (Inst _ _ _ _) = True
+ isInst _ = False
+
+ instantiate uid to (Inst idMap from fromTy toTy) dst
+ = trace ("inst " ++ show from ++ " ~> " ++ show to ++ " | " ++ show idMap)
+ $ let (gUID, lUID) = mkNewLevUID uid
+ (src, mCanonTy) = construct from idMap gUID
+ src' = fresh (sacred to ++ sacred from) (eqs' (fromTy : mCanonTy) toTy) src lUID
+ in dst ++ src'
+
+ -- sacred bndgId = Map.findWithDefault (error ("no sacred anns for binding group: " ++ show bndgId ++ " | " ++ show sacreds)) bndgId sacreds
+ sacred bndgId = Map.findWithDefault [] bndgId sacreds
+
+{-
+ fresh _ tups src
+ = concatMap eqs tups ++ src
+ where
+ eqs (a, b) = [a ::=>=:: b, b ::=>=:: a]
+-}
+ fresh sacs tups src uid
+ = let uidL = mkInfNewUIDL uid
+ anns (a ::=>=:: b) = [a, b]
+ anns (l ::<=:: a) = a : l
+ allAnns = nub (concatMap anns src)
+ fsubst = zipWith (\a u -> (a, repl a u)) allAnns uidL
+ tups' = map (\(f, t) -> (repl2 f f, repl2 t t)) tups
+ src' = map fr src
+
+ fr (a ::=>=:: b) = (repl2 a a) ::=>=:: (repl2 b b)
+ fr (l ::<=:: a) = (zipWith repl2 l l) ::<=:: (repl2 a a)
+
+ repl v u
+ | v `elem` sacs = v
+ | otherwise = u
+ repl2 v u
+ | isJust m = fromJust m
+ | otherwise = u
+ where
+ m = v `lookup` fsubst
+
+ eqs (a, b) = [a ::=>=:: b, b ::=>=:: a]
+ in concatMap eqs tups' ++ src'
+
+solve :: Bndgs -> Map UID [UID] -> UID -> UID -> Map UID Int
+solve bndgs sacred outerUID startUID
+ = let cs = flatten bndgs outerUID sacred
+ cs' = seq (length (show cs)) ( trace "flattening complete" cs)
+ in -- error (show sacred)
+ worklistFix upperSolveF 0 cs' $ Map.singleton startUID 1
+
+mkSacsMap :: [(UID, [UID])] -> Map UID [UID]
+mkSacsMap = foldr (uncurry (Map.insertWith (++))) Map.empty
+
+%%]
+
View
7 EHC/src/ehc/Ty/AbsSyn.cag
@@ -23,14 +23,19 @@ DATA TyAGItf
%%[1.Ty
DATA Ty
| Con nm : {HsName}
+ bndgs : BndgIdList
| App func : Ty
arg : Ty
| Any
+
+TYPE BndgIdList = [ Ty ]
%%]
%%[2.TyVar
DATA Ty
| Var tv : {TyVarId}
+ | Ann ann : {UID}
+ ty : Ty
%%]
%%[3.TyVar -2.TyVar
@@ -154,7 +159,7 @@ DATA Pred
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%[1.AllTy
-SET AllTyTy = Ty
+SET AllTyTy = Ty BndgIdList
SET AllTy = AllTyTy
SET AllTyAndFlds = AllTy
%%]
View
22 EHC/src/ehc/Ty/FitsIn.chs
@@ -29,7 +29,7 @@
%%[1 module {%{EH}Ty.FitsIn} import({%{EH}Base.Common}, {%{EH}Ty.FitsInCommon}, {%{EH}Ty}, {%{EH}Error}) export (fitsIn)
%%]
-%%[2 import({%{EH}Cnstr},{%{EH}Substitutable})
+%%[2 import({%{EH}Cnstr},{%{EH}Substitutable},Debug.Trace)
%%]
%%[4 import({%{EH}Ty.Instantiate}, {%{EH}Base.Opts}, {%{EH}Gam}, Data.Maybe,Data.List as List)
@@ -174,9 +174,13 @@ fitsIn ty1 ty2
%%[fitsInBotCon.1
f Ty_Any t2 = res t2 -- m.any.l
f t1 Ty_Any = res t1 -- m.any.r
- f t1@(Ty_Con s1) -- m.con
- t2@(Ty_Con s2)
- | s1 == s2 = res t2
+ f t1@(Ty_Con s1 bndgs1) -- m.con
+ t2@(Ty_Con s2 bndgs2)
+ | s1 == s2 = let pairs = zip bndgs1 bndgs2
+ foc = foldr (uncurry comb) emptyCnstr pairs
+ comb ta tb cnstr = foCnstr (f ta tb) |=> cnstr
+ in trace ("fitting: " ++ show bndgs1 ++ " with " ++ show bndgs2)
+ $ (res t2) { foCnstr = foc }
%%]
%%[fitsInBind.2
@@ -207,10 +211,10 @@ fitsIn ty1 ty2
%%]
%%[fitsInApp.1
- f t1@(Ty_App (Ty_App (Ty_Con c1) ta1) tr1) -- m.arrow
- t2@(Ty_App (Ty_App (Ty_Con c2) ta2) tr2)
- | hsnIsArrow c1 && c1 == c2
- = comp ta2 tr1 ta1 tr2 (\a r -> [a] `mkArrow` r)
+-- f t1@(Ty_App (Ty_App (Ty_Con c1) ta1) tr1) -- m.arrow
+-- t2@(Ty_App (Ty_App (Ty_Con c2) ta2) tr2)
+-- | hsnIsArrow c1 && c1 == c2
+-- = comp ta2 tr1 ta1 tr2 (\a r -> [a] `mkArrow` r)
f t1@(Ty_App tf1 ta1) -- m.prod
t2@(Ty_App tf2 ta2)
= comp tf1 ta1 tf2 ta2 Ty_App
@@ -571,7 +575,7 @@ fitsIn opts env uniq ty1 ty2
%%[10.fitsIn.fRow.foR -7.fitsIn.fRow.foR
fo = fR fi2 r1 r2 extsIn1 extsIn12 extsIn2
- foR = (if isRec then foUpdRecCoe (foCnstr fo |=> r1) (foCnstr fo |=> r2) extsIn1 extsIn12 extsIn2 else id) fo
+ foR = (if isRec then foUpdRecCoe (foCnstr fo |=> r1) (foCnstr fo |=> r2) extsIn1 extsIn12 extsIn2 else id) fo
foUpdRecCoe r1 r2 e1 e12 e2 fo
= let rn = uidHNm u1
prfCxId = fePrfCtxtId (fiEnv fi)
View
11 EHC/src/ehc/Ty/Pretty.cag
@@ -230,12 +230,16 @@ SEM Ty
ATTR TyAGItf AllTy [ | | pp USE {>#<} {empty}: PP_Doc ]
SEM Ty
- | Con loc . pp = ppCon @nm
+ | Con loc . pp = ppCon @nm >|< @bndgs.pp
| App loc . ppDflt = @func.pp >#< @arg.pp
. ppNice = ppParNeed @parNeed @lhs.parNeed
(ppAppTop (@appFunNm,@appFunPP) @appArgPPL @ppDflt)
. pp = if @isSpineRoot then @ppNice else @ppDflt
| Any loc . pp = pp hsnUnknown
+
+SEM BndgIdList
+ | Nil lhs . pp = empty
+ | Cons lhs . pp = "^" >|< @hd.pp >|< @tl.pp
%%]
%%[8
@@ -254,6 +258,7 @@ SEM Ty
%%[2.Var
SEM Ty
| Var loc . pp = pp ("v_" ++ show @tv)
+ | Ann loc . pp = pp ("d_" ++ show @ann) >|< ":" >|< @ty.pp
%%]
%%[3.Var -2.Var
@@ -452,6 +457,10 @@ SEM Ty
else (ParNotNeeded,@lhs.parNeedL)
(arg.parNeed,func.parNeedL)
= hdAndTl @argsParNeedL
+
+SEM BndgIdList
+ | Cons loc . parNeed = ParNotNeeded
+ . parNeedL = []
%%]
%%[3
View
150 EHC/src/ehc/rules/EhcRulesOrig.rul
@@ -247,7 +247,7 @@ format tex tFun = t.1
format tex tArg = t.2
format tex tyexprCon =
-format tex tyexprQuant =
+format tex tyexprQuant =
format ag tQu = qu
format ag tVar = tyVar
@@ -336,8 +336,8 @@ scheme expr "Expr" =
explain knTy = ("Expected/known" type of expression)
explain tyGam = (Environment | (ident :-> ty)..._ | for type identifiers, cannot be modified (hence treated as a global constant in "\\ruleRef{e.ann}"))
view C =
- holes [ | thread tyCnstr: Cnstr | ]
- judgespec kiGam ; tyGam ; valGam ; tyCnstr.inh ; knTy :- e : ty ~> tyCnstr.syn
+ holes [ bndgGam: ValGam | thread tyCnstr: Cnstr | retain annTy: Ty ]
+ judgespec bndgGam; kiGam ; tyGam ; valGam ; tyCnstr.inh ; knTy :- e : ty ~> tyCnstr.syn
judgeuse tex valGam ; tyCnstr.inh ; knTy :-.."e" e : ty ~> tyCnstr.syn
explain (Within environment |valGam| , expecting the type of expression |e| to be |tyCnstr.inh knTy| , |e| has type |ty| , under constraints |tyCnstr.syn| .)
explain tyCnstr.inh = (Already known constraints)
@@ -437,6 +437,7 @@ ruleset expr.base scheme expr "Expression type rules" =
judge F : fit
| cnstr = tyCnstr
| rty = tyCnstr.inh knTy
+ judge Ann : ann = ty ~> annTy
---
judge R : expr
| tyCnstr.syn = tyCnstr tyCnstr.inh
@@ -464,6 +465,9 @@ ruleset expr.base scheme expr "Expression type rules" =
judge F : fit
| lty = tyChar
---
+ view C =
+ judge Ann : ann = ty ~> annTy
+ ---
view I2 =
---
judge R : expr
@@ -487,6 +491,9 @@ ruleset expr.base scheme expr "Expression type rules" =
judge F : fit
| lty = tyString
---
+ view C =
+ judge Ann : ann = ty ~> annTy
+ ---
view I2 =
---
judge R : expr
@@ -510,6 +517,9 @@ ruleset expr.base scheme expr "Expression type rules" =
judge F : fit
| lty = tyFloat
---
+ view C =
+ judge Ann : ann = ty ~> annTy
+ ---
view I2 =
---
judge R : expr
@@ -582,10 +592,12 @@ ruleset expr.base scheme expr "Expression type rules" =
| rty = knTy
---
view C =
+ judge I : bndgIdInst = (tyCnstr.inh ty.g) :- ty.i ~> pairs
judge F : fit
- | lty = tyCnstr.inh ty.g
+ | lty = tyCnstr.inh ty.i
| rty = tyCnstr.inh knTy
| cnstr = tyCnstr
+ judge Ann : ann = ty ~> annTy
---
judge R : expr
| tyCnstr.syn = tyCnstr tyCnstr.inh
@@ -600,9 +612,9 @@ ruleset expr.base scheme expr "Expression type rules" =
judge - I
judge F : fit
| lty = tyCnstr.inh ty.g
- -
+ -
view I2 =
- -
+ -
judge R : expr
| ity = ityCnstr.inh ty.g
| ityCnstr.syn = ityCnstr.inh
@@ -616,14 +628,14 @@ ruleset expr.base scheme expr "Expression type rules" =
| translExpr = coe (translVar (ident) | TranslExpr)
rule e.con : e.var viewsel K - * "Con" =
- view K =
+ view K =
judge O: tyOpenProd = ty.p.._, n === ty.r
judge - G F
---
judge R : expr = kiGam ; tyGam ; valGam ; ((...) -> ty.r) :- "(,)" : (ty.p.._ -> ty.r)
view C =
- judge - G O
+ judge - G O I
judge V : tvarvFreshN = (`|` (identc | Nm) `|`) : tvarv..._
judge P : mkProdTy = ty.p === tvarv..._
judge F : fit
@@ -679,8 +691,10 @@ ruleset expr.base scheme expr "Expression type rules" =
---
view C =
judge V : tvarvFresh
+ judge AR : mkBndgArr = tvarv ; knTy :- bndgId ~> arr
+ judge AB : freshBndgId = bndgId
judge F : expr
- | knTy = tvarv -> knTy
+ | knTy = arr
| tyCnstr.syn = tyCnstr.fun
judge A : expr
| tyCnstr.inh = tyCnstr.fun
@@ -749,11 +763,11 @@ ruleset expr.base scheme expr "Expression type rules" =
| translExpr = \translExpr.f ^^ translExpr.a.._ ^^ translExpr.a
rule e.app.f : e.app viewsel I1 - * "AppImpred" =
- view I1 =
+ view I1 =
judge A : expr
| fiopt = strongFIOpts
---
- view I2 =
+ view I2 =
judge fitA : fit
| fiopt = impredFIOpts
---
@@ -824,8 +838,13 @@ ruleset expr.base scheme expr "Expression type rules" =
| knTy = tvarv1
| ty = ty.p
| patFunTy = _
+ judge AR1 : mkBndgArr = tvarv1 ; tvarv2 :- bndgId ~> arrTy
+ judge AR2 : mkBndgAnnArr = ty.p.in ; annTy.e :- bndgId ~> annTyPre
+ judge AB : freshBndgId = bndgId
+ judge BG : toBndgGam = bndgId :- "@arg.valGam2" ~> bndgGam.pat
+ judge Ann : ann = ty.p ~> ty.p.in
judge fitF : fit
- | lty = tvarv1 -> tvarv2
+ | lty = arrTy
| rty = tyCnstr.inh knTy
| cnstr = tyCnstr.fitF
| ty = _
@@ -834,10 +853,14 @@ ruleset expr.base scheme expr "Expression type rules" =
| tyCnstr.syn = tyCnstr.e
| knTy = tvarv2
| ty = ty.e
+ | bndgGam = bndgGam.pat + bndgGam.in
+ | annTy = annTy.e
---
judge R : expr
- | ty = tyCnstr.e ty.p -> ty.e
+ | ty = tyCnstr.e arrTy
| tyCnstr.syn = tyCnstr.e
+ | bndgGam = bndgGam.in
+ | annTy = "@lhs.finTyCnstr" |=> (annTyPre)
view I1 =
judge P : patexpr
| valGam.inh = (emptyGam|ValGam) ++ valGam
@@ -965,7 +988,7 @@ ruleset expr.base scheme expr "Expression type rules" =
judge G : predGamLookupPrTyEv = pred.a :> _ : ty.a `elem` valGam
judge prG : bind1PredToTy = predGam.i === [pred.a :> lamPat : ty.a]
judge P : patexpr = fiopt ; tyGam ; emptyGam ; emptyCnstr ; ty.a :- lamPat : _ ; tyGam.p ; patValGam ~> patTyCnstr ; _
- judge B : expr
+ judge B : expr
| knTy = ty.r
| valGam = predGam.i , patValGam , valGam
| e = lamBody
@@ -999,12 +1022,15 @@ ruleset expr.base scheme expr "Expression type rules" =
| patTyCnstr.inh = tyCnstr.inh
| tyCnstr.inh = patTyCnstr.syn
| tyCnstr.syn = tyCnstr.d
+ | bndgGam = bndgGamCol + bndgGam.in
judge B : expr
| tyCnstr.inh = tyCnstr.d
| tyCnstr.syn = tyCnstr.e
+ | bndgGam = bndgGamCol + bndgGam.in
---
judge R : expr
| tyCnstr.syn = tyCnstr.e
+ | bndgGam = bndgGam.in
view HM =
judge split : valGamPop = valGam.l ++ valGam.g === patValGam.syn
@@ -1156,7 +1182,7 @@ ruleset expr.onlyE scheme expr "Expression type rules" =
---
judge R : expr
| knTy = (knTy.1,knTy.2)
-
+
rule e.pred viewsel E - K =
view E =
judge P : pred = valGam :- pred
@@ -1192,8 +1218,8 @@ scheme decl "Decl" =
explain patValGam.syn = (|patValGam.inh| + new bindings)
explain tyGam = (Environment | (ident :-> ty)..._ | for type identifiers, cannot be modified (hence treated as a global constant in "\\ruleRef{e.ann}"))
view C =
- holes [ | thread tyCnstr: Cnstr, thread patTyCnstr: Cnstr | ]
- judgespec tySigGam ; patValGam.inh ; kiGam ; tyGam ; valGam ; patTyCnstr.inh ; tyCnstr.inh :- d : gathTySigGam ; patValGam.syn ~> patTyCnstr.syn ; tyCnstr.syn
+ holes [bndgGam:ValGam | thread tyCnstr: Cnstr, thread patTyCnstr: Cnstr | bndgGamCol:ValGam]
+ judgespec bndgGam; tySigGam ; patValGam.inh ; kiGam ; tyGam ; valGam ; patTyCnstr.inh ; tyCnstr.inh :- d : gathTySigGam ; patValGam.syn ~> patTyCnstr.syn ; tyCnstr.syn; bndgGamCol
judgeuse tex tySigGam ; patValGam.inh ; valGam ; patTyCnstr.inh ; tyCnstr.inh :-.."d" d : gathTySigGam ; patValGam.syn ~> patTyCnstr.syn ; tyCnstr.syn
explain (Declaration |d| has explicit type bindings |gathTySigGam| ,
within explicit bindings |tySigGam| and implicit type bindings |patTyCnstr.inh patValGam.inh| ,
@@ -1233,6 +1259,7 @@ ruleset decl.base scheme decl "Declaration type rules" =
judge R : decl
| patTyCnstr.syn = patTyCnstr.inh
| tyCnstr.syn = tyCnstr.inh
+ | bndgGamCol = emptyGam
view HM =
judge T : tyexpr
| tyWildL = tvarv.t.._
@@ -1261,14 +1288,14 @@ ruleset decl.base scheme decl "Declaration type rules" =
judge R : decl
| translBind = emptyTranslBind
- rule d.sig.val viewsel E =
+ rule d.sig.val viewsel E =
view E =
judge E : expr = kiGam ; tyGam ; valGam :- e.identv : ty.identv
judge B : bind1ValIdToTy = valGam.identv === [identv :-> ty.identv]
---
judge R : decl = kiGam ; tyGam ; valGam :- ((identv :: ty.identv ; identv `=` e.identv)) : valGam.identv
- rule d.val viewsel K - * "Val" =
+ rule d.val viewsel K - * "Val" =
view K =
judge L : valGamLookupPatTy = declPat :-> ty.sig `elem` tySigGam
judge P : patexpr = patValGam.inh ; ty.sig :- declPat : patValGam.syn
@@ -1287,7 +1314,11 @@ ruleset decl.base scheme decl "Declaration type rules" =
judge E : expr
| tyCnstr.syn = tyCnstr.e
| knTy = ty.e.k
- -
+ | ty = ty.e
+ judge B : freshBndgId = bndgId
+ judge BG : toBndgGam = bndgId :- "@patExpr.valGam2" ~> bndgGamCol
+ judge Ann : ann = ty.e ~> annTy.fresh
+ -
judge R : decl
| tyCnstr.syn = tyCnstr.e
view HM =
@@ -1410,7 +1441,7 @@ ruleset patexpr.base scheme patexpr viewsel K - * "Pattern expression type rules
judge F : fit
| rty = tyChar
---
- judge R : patexpr
+ judge R : patexpr
| p = char
view C =
---
@@ -1423,7 +1454,7 @@ ruleset patexpr.base scheme patexpr viewsel K - * "Pattern expression type rules
judge F : fit
| rty = tyString
---
- judge R : patexpr
+ judge R : patexpr
| p = str
view C =
---
@@ -1436,7 +1467,7 @@ ruleset patexpr.base scheme patexpr viewsel K - * "Pattern expression type rules
judge F : fit
| rty = tyFloat
---
- judge R : patexpr
+ judge R : patexpr
| p = float
view C =
---
@@ -1576,7 +1607,7 @@ ruleset patexpr.base scheme patexpr viewsel K - * "Pattern expression type rules
judge F : patexpr
| tyCnstr.syn = tyCnstr.f
judge A : patexpr
- | patFunTy = _
+ | patFunTy = _
| knTy = ty.a -- tyCnstr.f ty.a
| tyCnstr.syn = tyCnstr.a
| tyCnstr.inh = tyCnstr.f
@@ -1600,7 +1631,7 @@ ruleset patexpr.base scheme patexpr viewsel K - * "Pattern expression type rules
judge P : patexpr = fiopt ; tyGam.t ; valGam.inh ; (tyCnstr.f tyCnstr.inh) ; ty :- pExpr : ty.p ; tyGam.p ; valGam.p ~> tyCnstr.p ; _
---
judge R : patexpr = fiopt ; tyGam.inh ; valGam.inh ; tyCnstr.inh ; knTy :- (((node 2 = pExpr) :: (node 1 = tAnn))) : ty.p ; tyGam.p ; valGam.p ~> tyCnstr.p ; ANY
-
+
-------------------------------------------------------------------------
-- Type Expr
-------------------------------------------------------------------------
@@ -1732,7 +1763,7 @@ relation tyAltTyElim =
judgeuse ag (retain fo_altElim) `=` tyElimAlts (mkFitsInWrap' "@fe") fiopt tvarv.g.._ unique (ityCnstr.in ity)
| (retain ityCnstr ) `=` tyElimAltsCleanup ityCnstr.in (foCnstr "@fo_altElim")
| (retain ty ) `=` foTy "@fo_altElim"
- explain (Within a meet/join context (indicated by |fiopt|), known constraints |ityCnstr.in| for |ity| ,
+ explain (Within a meet/join context (indicated by |fiopt|), known constraints |ityCnstr.in| for |ity| ,
|ty| equals |ity| in which all type alternatives (except for global type variables |tvarv.g.._|) are eliminated,
under |ityCnstr| constraining the type alternative variables to their type alternive eliminated type.
)
@@ -2017,7 +2048,7 @@ ruleset match.all scheme match viewsel K - * "Type matching rules" =
judge O : fioptHasOpt = fioBindLFirstY `elem` fiopt
---
view I2 =
- judge O : fioptHasOpt
+ judge O : fioptHasOpt
| opt = fioBindToTyAltsN, fioBindLFirstY
---
view P =
@@ -2103,19 +2134,19 @@ ruleset match.all scheme match viewsel K - * "Type matching rules" =
judge I : inst.tvarv' = ty.i, tvarv, tvarv..._ === ty.1, alpha
---
judge R : match = fiopt :- (forall ^ alpha..._ `.` ty.1) <=>.(<=) ty.2 : ty ~> tyCnstr
-
+
rule m.forall.r viewsel I1 - * =
- view I1 =
+ view I1 =
judge F : match = fiopt :- ty.1 <=>.(<=) ty.i : ty ~> tyCnstr
judge I : inst.tvarv' = ty.i, tvarf, tvarf..._ === ty.2, alpha
---
- judge R : match = fiopt :- ty.1 <=>.(<=) (forall ^ alpha..._ `.` ty.2) : (tyCnstr (forall ^ alpha..._ `.` ty.2)) ~> tyCnstr
- view DT =
+ judge R : match = fiopt :- ty.1 <=>.(<=) (forall ^ alpha..._ `.` ty.2) : (tyCnstr (forall ^ alpha..._ `.` ty.2)) ~> tyCnstr
+ view DT =
judge O : fioptHasOpt = fioLeaveRInstN `elem` fiopt
---
-
+
rule m.forall.r2 viewsel DT - * =
- view DT =
+ view DT =
judge O : fioptHasOpt = fioLeaveRInstY `elem` fiopt
judge F : match = fiopt :- ty.1 <=>.(<=) ty.i : ty ~> tyCnstr
judge I : inst.tvarv' = ty.i, tvarv, tvarv..._ === ty.2, alpha
@@ -2128,7 +2159,7 @@ ruleset match.all scheme match viewsel K - * "Type matching rules" =
judge I : inst.tvarv' = ty.i, tcon, tcon..._ === ty.1, alpha
---
judge R : match = fiopt :- (exists ^ alpha..._ `.` ty.1) <=>.(<=) ty.2 : ty ~> tyCnstr
-
+
rule m.exists.r viewsel I1 - * =
view I1 =
judge F : match = fiopt :- ty.1 <=>.(<=) ty.i : ty ~> tyCnstr.f
@@ -2147,7 +2178,7 @@ ruleset match.all scheme match viewsel K - * "Type matching rules" =
judge I : inst.exists = ty.i === inst.exists(exists ^ alpha..._ `.` ty.2)
---
judge R : match = fiopt :- ty.1 <=>.(<=) (exists ^ alpha..._ `.` ty.2) : ty ~> tyCnstr
-
+
rule m.arrow =
view K =
judge Arg : match = :- ty.2.a <=>.(<=>) ty.1.a : ty.a
@@ -2193,7 +2224,7 @@ ruleset match.all scheme match viewsel K - * "Type matching rules" =
judge R : match
| cnstr = tyCnstr.r tyCnstr.l
| ty = (tyCnstr.r ty.l,ty.r)
-
+
rule m.alt viewsel I2 - * =
view I2 =
judge M : tyAltMk = ty === tvarv.2 [ (talt.1.._, talt.2.._) ]
@@ -2446,7 +2477,7 @@ relation valGamLookupPatTy =
)
)
)
-
+
view C =
judgeuse ag (pty,hasTySig)
`=` case ( ((pat).mbTopNm) of
@@ -3006,7 +3037,7 @@ relation tyAltPartition =
judgespec partitionTy === ty
relation tyAltSelect =
- view I2 =
+ view I2 =
holes [ tyAlts: TyPlusL, thard: TyHardness, tneed: TyNeed | | tys: TyL, tyElt: Ty ]
judgespec tys === tyAlts, tyElt, thard, tneed
judgeuse tex tys === [ tyElt `|` (tyElt :: thard / tneed) <- tyAlts ]
@@ -3080,3 +3111,46 @@ relation chkProdArity =
judgeuse ag (retain "loc.arityErrs") `=` (if length tyl == (pat).arity - then [] - else [Err_PatArity ty (pat).arity])
| (pat).knTyL `=` reverse tyl
+
+relation mkBndgArr =
+ view C =
+ holes [ tyP: Ty, tyR: Ty, bndgId: UID | | tyF: Ty ]
+ judgespec tyP ; tyR :- bndgId ~> tyF
+ judgeuse ag tyF `=` mkBndgArr (bndgId) (tyP) (tyR)
+
+relation mkBndgAnnArr =
+ view C =
+ holes [ tyP: Ty, tyR: Ty, bndgId: UID | | tyF: Ty ]
+ judgespec tyP ; tyR :- bndgId ~> tyF
+ judgeuse ag tyF `=` mkBndgAnnArr unique (bndgId) (tyP) (tyR)
+
+relation freshBndgId =
+ view C =
+ holes [ | | bndgId: UID ]
+ judgespec beta
+ judgeuse ag (retain bndgId) `=` unique
+
+relation arrToBndg =
+ view C =
+ holes [ty: Ty | | bndg: UID]
+ judgespec ty ~> bndg
+ judgeuse ag bndg `=` head (tyExtractBndgs ("@lhs.finTyCnstr" |=> (ty)))
+
+relation toBndgGam =
+ view C =
+ holes [valGam: ValGam, bndgId:UID | | bndgGam: ValGam]
+ judgespec bndgId :- valGam ~> bndgGam
+ judgeuse ag bndgGam `=` valGamToBndgGam (bndgId) (valGam)
+
+relation ann =
+ view C =
+ holes [ty: Ty | | annTy: Ty]
+ judgespec ty ~> annTy
+ judgeuse ag (retain annTy) `=` fst (tyAnnotate ("@lhs.finTyCnstr" |=> (ty)) unique)
+
+relation bndgIdInst =
+ view C =
+ holes [tyA: Ty | | tyB: Ty, retain pairs: Pairs ]
+ judgespec tyA :- tyB ~> pairs
+ judgeuse ag (tyB, pairs) `=` bndgIdInst unique (tyA)
+

No commit comments for this range

Something went wrong with that request. Please try again.