Permalink
Browse files

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.
  • Loading branch information...
amiddelk committed Sep 14, 2006
1 parent ad79d0a commit f1915d88be20dfce540973374c15ecd1d2a4c619
View
@@ -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
@@ -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
%%]
-
@@ -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})
@@ -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
@@ -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
@@ -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 ]
+%%]
+
Oops, something went wrong.

0 comments on commit f1915d8

Please sign in to comment.