lang-types.sml 9.38 KB
Newer Older
1
2
3
4
5
6
7
structure Types = struct

   structure BD = BooleanDomain

   type tvar = TVar.tvar
   type varset = TVar.set
   val freshTVar = TVar.freshTVar
Axel Simon's avatar
Axel Simon committed
8

Axel Simon's avatar
Axel Simon committed
9
   val concisePrint = true
Axel Simon's avatar
Axel Simon committed
10

11
   datatype texp =
12
13
      (* a function taking at least one argument *)
      FUN of (texp list * texp)
14
15
16
17
18
19
20
21
22
23
24
      (* a type synoym with its expanded type *)
    | SYN of (TypeInfo.symid * texp)
      (* an whole number *)
    | ZENO
      (* a floating point number *)
    | FLOAT
      (* a value containing no information *)
    | UNIT
      (* a bit vector of a fixed size *)
    | VEC of texp
      (* a Herbrand constant, can only occur as the argument of VEC *)
Axel Simon's avatar
Axel Simon committed
25
    | CONST of int
26
27
28
      (* an algebraic data type with a list of type arguments *)
    | ALG of (TypeInfo.symid * texp list)
      (* a record *)
Axel Simon's avatar
Axel Simon committed
29
    | RECORD of (TVar.tvar * BD.bvar * rfield list)
30
31
      (* the state monad: return value, input state, output state *)
    | MONAD of texp * texp * texp
32
      (* a type variable *)
Axel Simon's avatar
Axel Simon committed
33
    | VAR of TVar.tvar * BD.bvar
34
35
 
   and rfield = RField of {
Axel Simon's avatar
Axel Simon committed
36
37
38
      name : FieldInfo.symid,
      fty : texp,
      exists : BooleanDomain.bvar
39
40
   }

41
42
43
44
45
46
47
48
49
50
   exception LangTypesBug
              
   fun newFlow (VAR (a,_)) = VAR (a, BD.freshBVar ())
     | newFlow _ = raise LangTypesBug
   fun freshVar () = VAR (freshTVar (), BD.freshBVar ())
   fun bvar (VAR (v,b)) = b
     | bvar _ = raise LangTypesBug
   fun tvar (VAR (v,b)) = v
     | tvar _ = raise LangTypesBug      

51
   fun texpVarset (e, vs) = let
52
      fun tV (FUN (f1, f2), vs) = tV (f2, List.foldl tV vs f1)
53
54
55
56
57
58
59
        | tV (SYN (syn, t), vs) = tV (t, vs)
        | tV (ZENO, vs) = vs
        | tV (FLOAT, vs) = vs
        | tV (UNIT, vs) = vs
        | tV (VEC t, vs) = tV (t, vs)
        | tV (CONST c, vs) = vs
        | tV (ALG (ty, l), vs) = List.foldl tV vs l
Axel Simon's avatar
Axel Simon committed
60
        | tV (RECORD (v,_,l), vs) = List.foldl tVF (TVar.add (v,vs)) l
61
        | tV (MONAD (r,f,t), vs) = tV (r, tV (f, tV (t, vs)))
Axel Simon's avatar
Axel Simon committed
62
63
        | tV (VAR (v,_), vs) = TVar.add (v,vs)
      and tVF (RField {name = n, fty = t, exists = b}, vs) = tV (t,vs)
64
65
      in (tV (e, vs))
   end
66

Axel Simon's avatar
Axel Simon committed
67
   (*gather Boolean flags, the collection function is generic and is passed a
Axel Simon's avatar
Axel Simon committed
68
   bool that is true if the flag is in a contra-variant position*)
69
   fun texpBVarset cons (e, bs) = let
70
      fun tV co (FUN (f1, f2), bs) = tV co (f2, List.foldl (tV (not co)) bs f1)
71
72
73
74
75
76
77
        | tV co (SYN (syn, t), bs) = tV co (t, bs)
        | tV co (ZENO, bs) = bs
        | tV co (FLOAT, bs) = bs
        | tV co (UNIT, bs) = bs
        | tV co (VEC t, bs) = tV co (t, bs)
        | tV co (CONST c, bs) = bs
        | tV co (ALG (ty, l), bs) = List.foldl (tV co) bs l
Axel Simon's avatar
Axel Simon committed
78
        | tV co (RECORD (v,b,l), bs) =
Axel Simon's avatar
Axel Simon committed
79
            cons ((co,b), List.foldl (tVF co) bs l)
Axel Simon's avatar
Axel Simon committed
80
81
        | tV co (MONAD (r,f,t), bs) =
         tV co (r, tV (not co) (f, tV co (t, bs)))
Axel Simon's avatar
Axel Simon committed
82
        | tV co (VAR (v,b), bs) = cons ((co,b),bs)
83
      and tVF co (RField {name = n, fty = t, exists = b}, bs) =
Axel Simon's avatar
Axel Simon committed
84
         cons ((co,b), tV co (t, bs))
85
86
87
88
      in (tV false (e, bs))
   end

   fun fieldBVarsets (e, pn) = let
89
      fun tV pn (FUN (f1, f2)) = tV (List.foldl (fn (t,pn) => tV pn t) pn f1) f2
90
91
92
93
94
95
96
97
98
        | tV pn (SYN (syn, t)) = tV pn t
        | tV pn (ZENO) = pn
        | tV pn (FLOAT) = pn
        | tV pn (UNIT) = pn
        | tV pn (VEC t) = tV pn t
        | tV pn (CONST c) = pn
        | tV pn (ALG (ty, l)) = List.foldl (fn (t,pn) => tV pn t) pn l
        | tV (p,n) (RECORD (_,b,l)) = 
            List.foldl (fn (f,pn) => tVF pn f) (p, BD.addToSet (b,n)) l
99
        | tV pn (MONAD (r,f,t)) = tV (tV (tV pn r) f) t
100
101
102
103
104
105
106
107
        | tV (p,n) (VAR (_,b)) = (p, BD.addToSet(b,n))
      and tVF (p,n) (RField {name, fty = t, exists = b}) =
         tV (BD.addToSet (b,p), n) t
      in (tV pn e)
   end

   fun fieldOfBVar (v, e) = let
      fun takeIfSome (t,fo) = case ff t of SOME f => SOME f | NONE => fo
108
109
110
111
      and ff (FUN (f1, f2)) = takeIfSome (f2,
            case List.mapPartial ff f1 of
               (f :: _) => SOME f
             | [] => NONE)
112
113
114
115
116
117
118
119
120
121
        | ff (SYN (syn, t)) = ff t
        | ff (ZENO) = NONE
        | ff (FLOAT) = NONE
        | ff (UNIT) = NONE
        | ff (VEC t) = ff t
        | ff (CONST c) = NONE
        | ff (ALG (ty, l)) = List.foldl takeIfSome NONE l
        | ff (RECORD (_,b,l)) = (case List.mapPartial ffF l of
              (f :: _) => SOME f
            | [] => NONE)
122
        | ff (MONAD (r,f,t)) = takeIfSome (r, (takeIfSome (f,ff t)))
123
124
125
126
127
128
        | ff (VAR (b,_)) = NONE
      and ffF (RField {name = n, fty = t, exists = b}) =
         if BD.eq(v,b) then SOME n else ff t
      in ff e
   end

129
   fun setFlagsToTop (FUN (f1, f2)) = FUN (List.map setFlagsToTop f1, setFlagsToTop f2)
130
131
132
133
134
135
136
137
138
     | setFlagsToTop (SYN (syn, t)) = SYN (syn, setFlagsToTop t)
     | setFlagsToTop (ZENO) = ZENO
     | setFlagsToTop (FLOAT) = FLOAT
     | setFlagsToTop (UNIT) = UNIT
     | setFlagsToTop (VEC t) = VEC (setFlagsToTop t)
     | setFlagsToTop (CONST c) = CONST c
     | setFlagsToTop (ALG (ty, l)) = ALG (ty, List.map setFlagsToTop l)
     | setFlagsToTop (RECORD (var, b, l)) =
         RECORD (var, BD.freshBVar (), List.map setFlagsToTopF l)
139
140
     | setFlagsToTop (MONAD (r,f,t)) =
         MONAD (setFlagsToTop r, setFlagsToTop f, setFlagsToTop t)
141
142
143
144
145
     | setFlagsToTop (VAR (var,b)) = VAR (var, BD.freshBVar ())
   and
     setFlagsToTopF (RField {name = n, fty = t, exists = _}) =
        RField {name = n, fty = setFlagsToTop t, exists = BD.freshBVar ()}

146
147
148
149
   fun replaceTVars (e, vs) = let
      fun chg v = case List.find (fn (v1,_) => TVar.eq(v,v1)) vs of
           NONE => v
         | SOME (v1,v2) => v2
150
      fun repl (FUN (f1, f2)) = FUN (List.map repl f1, repl f2)
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
        | repl (SYN (syn, t)) = SYN (syn, repl t)
        | repl (ZENO) = ZENO
        | repl (FLOAT) = FLOAT
        | repl (UNIT) = UNIT
        | repl (VEC t) = VEC (repl t)
        | repl (CONST c) = CONST c
        | repl (ALG (ty, l)) = ALG (ty, List.map repl l)
        | repl (RECORD (v,bv,l)) = RECORD (chg v, bv, List.map replF l)
        | repl (MONAD (r,f,t)) = MONAD (repl r, repl f, repl t)
        | repl (VAR (v,bv)) = VAR (chg v,bv)
      and replF (RField {name = n, fty = t, exists = b}) =
         RField {name = n, fty = repl t, exists = b}
      in repl e
   end

166
167
168
169
   fun replaceBVars (e, vs) = let
      fun chg v = case List.find (fn (v1,_) => BD.eq(v,v1)) vs of
           NONE => v
         | SOME (v1,v2) => v2
170
      fun repl (FUN (f1, f2)) = FUN (List.map repl f1, repl f2)
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
        | repl (SYN (syn, t)) = SYN (syn, repl t)
        | repl (ZENO) = ZENO
        | repl (FLOAT) = FLOAT
        | repl (UNIT) = UNIT
        | repl (VEC t) = VEC (repl t)
        | repl (CONST c) = CONST c
        | repl (ALG (ty, l)) = ALG (ty, List.map repl l)
        | repl (RECORD (v,bv,l)) = RECORD (v, chg bv, List.map replF l)
        | repl (MONAD (r,f,t)) = MONAD (repl r, repl f, repl t)
        | repl (VAR (v,bv)) = VAR (v,chg bv)
      and replF (RField {name = n, fty = t, exists = b}) =
         RField {name = n, fty = repl t, exists = chg b}
      in repl e
   end

186
187
188
189
190
   fun compare_rfield (RField f1, RField f2) =
     SymbolTable.compare_symid (#name f1, #name f2)

   type condescr = texp option SymMap.map

191
   type typedescr = { tdVars : (tvar * BD.bvar) list,
192
193
194
195
                     tdCons : condescr }

   fun showTypeSI (ty, showInfo) = let
    val siTab = ref showInfo
Axel Simon's avatar
Axel Simon committed
196
197
198
    fun sep s [] = ""
      | sep s [v] = v
      | sep s (v :: vs) = v ^ s ^ sep s vs
Axel Simon's avatar
Axel Simon committed
199
200
    fun br (curPrec, existsPrec,str) =
      if curPrec>existsPrec then "(" ^ str ^ ")" else str
Axel Simon's avatar
Axel Simon committed
201
202
    val p_app = 9
    val p_tyn = 10
203
    fun sT (p, FUN ([f1], f2)) =
204
          br (p, p_app, sT (p_app+1, f1) ^ " -> " ^ sT (p_app, f2))
205
206
207
      | sT (p, FUN (f1, f2)) =
          br (p, p_app, "(" ^ sep ", " (List.map (fn f => sT (0, f)) f1) ^
                        ") -> " ^ sT (p_app, f2))
208
209
210
211
212
213
      | sT (p, SYN (syn, t)) = 
          br (p, p_tyn, SymbolTable.getString(!SymbolTables.typeTable, syn))
      | sT (p, ZENO) = "int"
      | sT (p, FLOAT) = "float"
      | sT (p, UNIT) = "()"
      | sT (p, VEC t) = "[" ^ sT (0, t) ^ "]"
Axel Simon's avatar
Axel Simon committed
214
      | sT (p, CONST c) = Int.toString(c)
215
216
217
218
219
220
      | sT (p, ALG (ty, l)) = let
          val conStr = SymbolTable.getString(!SymbolTables.typeTable, ty)
          in if List.null l then conStr else br (p, p_tyn,
            List.foldl (fn (s1,s2) => s1 ^ " " ^ s2) conStr (
              List.map (fn e => sT (p_tyn+1, e)) l))
          end
Axel Simon's avatar
Axel Simon committed
221
      | sT (p, RECORD (v,b,l)) = "{" ^ List.foldl (op ^) "" (List.map sTF l) ^
Axel Simon's avatar
Axel Simon committed
222
223
224
                                   showVar v ^ 
                                   (if concisePrint then "" else BD.showVar b)
                                   ^ ":...}"
Axel Simon's avatar
Axel Simon committed
225
      | sT (p, MONAD (r,f,t)) = br (p, p_tyn, "S " ^ sT (p_tyn+1, r)) ^
Axel Simon's avatar
Axel Simon committed
226
         " <" ^ sT (p_app+1, f) ^ " => " ^ sT (p_app, t) ^ ">"
Axel Simon's avatar
Axel Simon committed
227
228
      | sT (p, VAR (v,b)) = showVar v ^ 
            (if concisePrint then "" else BD.showVar b)
229
230
231
232
233
   and showVar var = let 
         val (str, newSiTab) = TVar.varToString (var, !siTab)
      in
         (siTab := newSiTab; str)
      end
Axel Simon's avatar
Axel Simon committed
234
235
    and sTF (RField {name = n, fty = t, exists = b}) =
            SymbolTable.getString(!SymbolTables.fieldTable, n) ^
Axel Simon's avatar
Axel Simon committed
236
237
            (if concisePrint then "" else BD.showVar b)  ^
            ": " ^ sT (0, t) ^ ", "
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
    in (sT (0, ty), !siTab) 
   end

   fun showType ty =
      let val (str,_) = showTypeSI (ty, TVar.emptyShowInfo) in str end

   fun showTypes l = let
         fun sT (si, []) = ""
           | sT (si, (str, t) :: l) = (case showTypeSI (t, si) of
                  (tStr, si) => str ^ tStr ^ sT (si, l)
              )
         in
           sT (TVar.emptyShowInfo, l)
         end

end