Elaborate.hs 5.49 KB
Newer Older
1
module Elaborate where
2

3
4
5
import           FCoBase
import qualified FiPlusBase as FP
import qualified FiImpl as FIm
6

7
8
9
10
varTranslate :: FP.Variable -> Variable
varTranslate FP.Z              = Z
varTranslate (FP.STermVar var) = STermVar (varTranslate var)
varTranslate (FP.STypeVar var) = STypeVar (varTranslate var)
11

12
13
14
15
16
17
18
getTypeFromEnv :: FIm.Env -> FP.Variable -> Either String FP.FiType
getTypeFromEnv (FIm.ETermVar ty _) FP.Z = return ty
getTypeFromEnv _ FP.Z = Left "wrong or no binding for FiTerm"
getTypeFromEnv (FIm.ETermVar _ rest) (FP.STermVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (FP.STermVar h) = Left "wrong FiTerm binding"
getTypeFromEnv (FIm.ETypeVar _ rest) (FP.STypeVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (FP.STypeVar h) = Left "No variable FP.FiType"
19

20
21
22
23
24
25
26
27
elaborate :: FP.FiTerm -> FIm.Env -> Either String Term
elaborate FP.TmTop ctx = return TmTop
elaborate (FP.TmInt i) ctx = return (TmInt i)
elaborate (FP.TmVar hnat) ctx = return (TmVar (varTranslate hnat))
elaborate (FP.TmAbs t ty) ctx = do
  term <- elaborate t (FIm.ETermVar ty ctx)
  return (TmAbs term (convertType ty))
elaborate (FP.TmApp t1 t2) ctx = do
28
29
  term1 <- elaborate t1 ctx
  term2 <- elaborate t2 ctx
30
31
32
33
34
  ty2 <- FIm.typeOf t2 ctx
  case FIm.typeOf t1 ctx of
    Right (FP.TyArr ty3 ty4) -> do
      a <- (algoSubtypingCo FIm.EmptyQueue ty2 ty3)
      return (TmApp term1 (TmCast a term2))
35
    _ -> Left "Wrong use of elaborate"
36
elaborate (FP.TmMerge t1 t2) ctx = do
37
38
  term1 <- elaborate t1 ctx
  term2 <- elaborate t2 ctx
39
40
  return (TmTuple term1 term2)
elaborate (FP.TmRecord t str) ctx = do
41
42
  term <- elaborate t ctx
  return term
43
elaborate (FP.TmProj t str) ctx = do
44
45
  term <- elaborate t ctx
  return term
46
47
elaborate (FP.TmAnn t ty) ctx = do
  tyt <- FIm.typeOf t ctx
48
  term <- elaborate t ctx
49
  sub <- (algoSubtypingCo FIm.EmptyQueue tyt ty)
50
  return (TmCast sub term)
51
elaborate (FP.TypeApp t ty) ctx = do
52
  term <- elaborate t ctx
53
54
55
56
  return (TmTApp term (convertType ty))
elaborate (FP.TmAll ty t) ctx = do
  term <- elaborate t (FIm.ETypeVar ty ctx)
  return (TmTAbs term)
57

58
59
60
61
62
63
64
65
66
convertType :: FP.FiType -> Type
convertType FP.TyInt           = TyInt
convertType (FP.TyAnd ty1 ty2) = TyProd (convertType ty1) (convertType ty2)
convertType FP.TyBot           = TyAll (TyVar Z)
convertType FP.TyTop           = TyTop
convertType (FP.TyRecord ty _) = convertType ty
convertType (FP.TyVar hnat)    = TyVar (varTranslate hnat)
convertType (FP.TyArr ty1 ty2) = TyArr (convertType ty1) (convertType ty2)
convertType (FP.TyAll ty tyB)  = TyAll (convertType tyB)
67

68
69
70
71
72
pushQueue :: FIm.Queue -> FIm.Queue -> FIm.Queue
pushQueue FIm.EmptyQueue q              = q
pushQueue (FIm.LabelQueue str q) newq   = FIm.LabelQueue str (pushQueue q newq)
pushQueue (FIm.TypeQueue ty q) newq     = FIm.TypeQueue ty (pushQueue q newq)
pushQueue (FIm.TypeStarQueue ty q) newq = FIm.TypeStarQueue ty (pushQueue q newq)
73

74
75
76
77
78
isTypeConstant :: FP.FiType -> Bool
isTypeConstant FP.TyInt     = True
isTypeConstant FP.TyBot     = True
isTypeConstant (FP.TyVar _) = True
isTypeConstant _            = False
79

80
81
algoSubtypingCo :: FIm.Queue -> FP.FiType -> FP.FiType -> Either String Coercion
algoSubtypingCo q tyA FP.TyTop = do
82
83
  a <- (calcQueueTop q)
  return (CoTrans a (CoTop))
84
algoSubtypingCo q tyA (FP.TyAnd ty1 ty2) = do
85
86
87
88
  a <- (algoSubtypingCo q tyA ty1)
  b <- (algoSubtypingCo q tyA ty2)
  c <- (calcQueueAnd q)
  return (CoTrans c (CoTuple a b))
89
90
91
algoSubtypingCo q tyA (FP.TyArr ty1 ty2) =
  algoSubtypingCo (pushQueue q (FIm.TypeQueue ty1 FIm.EmptyQueue)) tyA ty2
algoSubtypingCo FIm.EmptyQueue tyA tyB
92
  | tyA == tyB && isTypeConstant tyA = return CoId
93
algoSubtypingCo q FP.TyBot c
94
  | isTypeConstant c = return CoBot
95
96
97
98
99
algoSubtypingCo q tyA (FP.TyRecord tyB str) =
  algoSubtypingCo (pushQueue q (FIm.LabelQueue str FIm.EmptyQueue)) tyA tyB
algoSubtypingCo q tyA (FP.TyAll ty1 ty2) =
  algoSubtypingCo (pushQueue q (FIm.TypeStarQueue ty1 FIm.EmptyQueue)) tyA ty2
algoSubtypingCo (FIm.TypeQueue ty q) (FP.TyArr ty1 ty2) tyB
100
  | isTypeConstant tyB = do
101
    a <- (algoSubtypingCo FIm.EmptyQueue ty ty1)
102
103
    b <- (algoSubtypingCo q ty2 tyB)
    return (CoArrow a b)
104
algoSubtypingCo (FIm.LabelQueue str1 q) (FP.TyRecord ty2 str2) tyB
105
  | isTypeConstant tyB && str1 == str2 = algoSubtypingCo q ty2 tyB
106
107
algoSubtypingCo q (FP.TyAnd ty1 ty2) tyB
  | isTypeConstant tyB && FIm.algoSubtyping q ty1 tyB = do
108
109
    a <- (algoSubtypingCo q ty1 tyB)
    return (CoTrans a (CoProj1))
110
  | isTypeConstant tyB && FIm.algoSubtyping q ty2 tyB = do
111
112
    a <- (algoSubtypingCo q ty2 tyB)
    return (CoTrans a (CoProj2))
113
algoSubtypingCo (FIm.TypeStarQueue ty q) (FP.TyAll ty1 ty2) tyB
114
115
116
117
118
  | isTypeConstant tyB = do
    a <- (algoSubtypingCo q ty2 tyB)
    return (CoAll a)
algoSubtypingCo _ _ _ = Left "no subtype"

119
120
121
calcQueueTop :: FIm.Queue -> Either String Coercion
calcQueueTop FIm.EmptyQueue = return CoTop
calcQueueTop (FIm.LabelQueue _ q) = do
122
123
  a <- (calcQueueTop q)
  return (CoTrans a CoId)
124
calcQueueTop (FIm.TypeQueue _ q) = do
125
126
  a <- (calcQueueTop q)
  return (CoTrans (CoArrow CoTop a) CoTopArrow)
127
calcQueueTop (FIm.TypeStarQueue _ q) = do
128
129
130
  a <- (calcQueueTop q)
  return (CoTrans (CoAll a) CoTopAll)

131
132
133
calcQueueAnd :: FIm.Queue -> Either String Coercion
calcQueueAnd FIm.EmptyQueue = return CoTop
calcQueueAnd (FIm.LabelQueue _ q) = do
134
135
  a <- (calcQueueAnd q)
  return (CoTrans a CoId)
136
calcQueueAnd (FIm.TypeQueue _ q) = do
137
138
  a <- (calcQueueAnd q)
  return (CoTrans (CoArrow CoId a) CoDistArrow)
139
calcQueueAnd (FIm.TypeStarQueue _ q) = do
140
141
142
143
  a <- (calcQueueAnd q)
  return (CoTrans (CoAll a) CoDistAll)

goodelaborate term = do
144
145
  ty <- FIm.typeOf term FIm.Nil
  elaborate term FIm.Nil