environment.sml 57.1 KB
Newer Older
1
2
structure Environment : sig
   type environment
3

Axel Simon's avatar
Axel Simon committed
4
5
   structure SpanMap : ORD_MAP where type Key.ord_key = Error.span

Axel Simon's avatar
Axel Simon committed
6
7
   structure SymbolSet : ORD_SET where type Key.ord_key = SymbolTable.symid
   
8
   datatype symbol_type =
Axel Simon's avatar
Axel Simon committed
9
10
11
        VALUE of {symType : Types.texp, symFlow : BooleanDomain.bfun}
      | DECODE of {symType : Types.texp, symFlow : BooleanDomain.bfun,
                   width : Types.texp}
12

13
14
15
   val primitiveEnvironment : (SymbolTable.symid *
                               Types.texp *
                               (BooleanDomain.bfun -> BooleanDomain.bfun) *
Axel Simon's avatar
Axel Simon committed
16
17
18
                               (Types.texp option)) list *
                               SizeConstraint.size_constraint list ->
                               environment
Axel Simon's avatar
Axel Simon committed
19
20
21
22
   
   val pushSingle : VarInfo.symid * Types.texp * environment -> environment
   
   (*add a group of bindings to the current environment, each element in a
Axel Simon's avatar
Axel Simon committed
23
24
25
   binding is identified by its symbol, the flag is true if the symbol
   is a decoder function*)
   val pushGroup : (VarInfo.symid * bool) list * environment ->
Axel Simon's avatar
Axel Simon committed
26
                  environment
27
28
29
30
   (*remove a binding group from the stack; the flag is true if the outermost
   scope should be kept, the result is a list of error messages about
   ambiguous type variables and a list with types of the symbols in this
   group*)
31
   val popGroup : environment * bool ->
Axel Simon's avatar
Axel Simon committed
32
                  (Error.span * string) list * environment
Axel Simon's avatar
Axel Simon committed
33
   val pushTop : environment -> environment
34
35
36
37
38
   
   (*pushes the given type onto the stack, if the flag is true, type variables
   are renamed*)
   val pushType : bool * Types.texp * environment -> environment

39
40
   val pushMonadType : Types.texp * environment -> environment
   
Axel Simon's avatar
Axel Simon committed
41
42
   (* push the width of a decode onto the stack*)
   val pushWidth : VarInfo.symid * environment -> environment
43

Axel Simon's avatar
Axel Simon committed
44
   (*given an occurrence of a symbol at a position, push its type onto the
Axel Simon's avatar
Axel Simon committed
45
46
   stack and return if an instance of this type must be used; arguments are
   the symbol to look up, the position it occurred and a list of symbols that
Axel Simon's avatar
Axel Simon committed
47
48
   denote the current context/function (the latter is ignored if the symbol
   already has a type) *)
49
   val pushSymbol : VarInfo.symid * Error.span * environment -> environment
Axel Simon's avatar
Axel Simon committed
50

Axel Simon's avatar
Axel Simon committed
51
52
   val getUsages : VarInfo.symid * environment -> Error.span list
   
Axel Simon's avatar
Axel Simon committed
53
54
55
   val getContextOfUsage : VarInfo.symid * Error.span * environment ->
                           VarInfo.symid list

56
57
58
59
   val getCtxt : environment -> VarInfo.symid list

      (*stack: [...,t] -> [...] and type of f for call-site s is set to t*)
   val popToUsage : VarInfo.symid * Error.span * VarInfo.symid list * environment ->
60
                    VarInfo.symid list * environment
Axel Simon's avatar
Axel Simon committed
61

62
63
64
   (*stack: [...] -> [...,t] where t is type of usage of f at call-site s,
     returns a list of functions whose types have changed (and that are
     still in scope)*)
Axel Simon's avatar
Axel Simon committed
65
   val pushUsage : VarInfo.symid * Error.span *
Axel Simon's avatar
Axel Simon committed
66
67
                   (VarInfo.symid * symbol_type) list * environment ->
                   environment
Axel Simon's avatar
Axel Simon committed
68
   
69
   (*stack: [...] -> [..., x:a], 'a' fresh; primed version also returns 'a'*)
70
   val pushLambdaVar' : VarInfo.symid * environment -> (Types.texp * environment)
71
72
   val pushLambdaVar : VarInfo.symid * environment -> environment
   
73
74
75
76
   (*stack: [..., t0, t1, ... tn] -> [..., {f1:t1, ... fn:tn, t0:...}]*)
   val reduceToRecord : (BooleanDomain.bvar * FieldInfo.symid) list *
                        environment -> environment

Axel Simon's avatar
Axel Simon committed
77
78
79
   (*stack: [..., tn, ..., t2, t1, t0] -> [..., SUM (tn,..t0)]*)
   val reduceToSum : int * environment -> environment
   
80
81
   (*stack: [...,t1,t2,...,tn] -> [...,(t1, ... t n-1) -> t2]*)
   val reduceToFunction : environment * int -> environment
82
   
83
   (*stack: [...,t1 -> t2] -> [...t2]*)
84
   val reduceToResult : environment -> environment
85
86
87
88
89
90

   (*stack: [..., tn, ..., t2, t1, t0] -> [..., t0]*)
   val return : int * environment -> environment

   val popKappa : environment -> environment

Axel Simon's avatar
Axel Simon committed
91
   (*stack: [...,t] -> [...] and type of function f is set to t*)
92
   val popToFunction : VarInfo.symid * environment -> environment
Axel Simon's avatar
Axel Simon committed
93
94
95

   (*the type of function f is unset*)
   val clearFunction : VarInfo.symid * environment -> environment
Axel Simon's avatar
Axel Simon committed
96
   
97
98
99
100
101
   (*add the given function symbol to the current context*)
   val pushFunction : VarInfo.symid * environment -> environment

   (*as above, additionally push a function type if it is set, otherwise push
   top*)
102
   val pushFunctionOrTop : VarInfo.symid * environment -> environment
Axel Simon's avatar
Axel Simon committed
103
   
104
105
106
107
108
   val forceNoInputs : VarInfo.symid * environment -> FieldInfo.symid list

    (*apply the Boolean function*)
   val meetBoolean : (BooleanDomain.bfun -> BooleanDomain.bfun) *
         environment -> environment
109

Axel Simon's avatar
Axel Simon committed
110
111
112
113
   val meetSizeConstraint : (SizeConstraint.size_constraint_set ->
                             SizeConstraint.size_constraint_set) *
                             environment -> environment

Axel Simon's avatar
Axel Simon committed
114
115
   val meetFlow : environment * environment -> environment
   val meet : environment * environment -> environment
Axel Simon's avatar
Axel Simon committed
116

Axel Simon's avatar
Axel Simon committed
117
118
119
   (*returns the set of substitutions for the first environment, this is empty
   if the the first environment is more specific (smaller) than the second*)
   val subseteq : environment * environment -> Substitutions.Substs
Axel Simon's avatar
Axel Simon committed
120
121
122
123

   (*query all function symbols in binding groups that would be modified by
   the given substitutions*)
   val affectedFunctions : Substitutions.Substs * environment -> SymbolSet.set
Axel Simon's avatar
Axel Simon committed
124
125
126

   val getFunctionInfo : VarInfo.symid * environment -> symbol_type

Axel Simon's avatar
Axel Simon committed
127
   val toString : environment -> string
Axel Simon's avatar
Axel Simon committed
128
   val toStringSI : environment * TVar.varmap -> string * TVar.varmap
129
   val topToString : environment -> string
130
   val topToStringSI : environment * TVar.varmap -> string * TVar.varmap
Axel Simon's avatar
Axel Simon committed
131
   val kappaToStringSI : environment * TVar.varmap -> string * TVar.varmap
132
133
   val funTypeToStringSI  : environment * VarInfo.symid * TVar.varmap ->
                            string * TVar.varmap
134
135
136
end = struct
   structure ST = SymbolTable
   structure BD = BooleanDomain
Axel Simon's avatar
Axel Simon committed
137
   structure SC = SizeConstraint
138
   structure SpanMap = SpanMap
139
   open Types
Axel Simon's avatar
Axel Simon committed
140
   open Substitutions
141

Axel Simon's avatar
Axel Simon committed
142
   (*any error that is not due to unification*)
143
   exception InferenceBug
144
145
146
   
   datatype bind_info
      = SIMPLE of { ty : texp }
147
      | COMPOUND of { ty : (texp * BD.bfun) option, width : texp option,
Axel Simon's avatar
Axel Simon committed
148
                     uses : (ST.symid list * texp) SpanMap.map }
149
150
151
152

   datatype binding
      = KAPPA of {
         ty : texp
Axel Simon's avatar
Axel Simon committed
153
      } | SINGLE of {
154
155
         name : ST.symid,
         ty : texp
Axel Simon's avatar
Axel Simon committed
156
      } | GROUP of {
157
         name : ST.symid,
Axel Simon's avatar
Axel Simon committed
158
         (*the type of this function, NONE if not yet known*)
159
         ty : (texp * BD.bfun) option,
Axel Simon's avatar
Axel Simon committed
160
161
         (*this is SOME (CONST w) if this is a decode function with pattern width w*)
         width : texp option,
Axel Simon's avatar
Axel Simon committed
162
         uses : (ST.symid list * texp) SpanMap.map
163
164
      } list
   
165
   datatype symbol_type =
Axel Simon's avatar
Axel Simon committed
166
167
168
        VALUE of {symType : Types.texp, symFlow : BooleanDomain.bfun}
      | DECODE of {symType : Types.texp, symFlow : BooleanDomain.bfun,
                   width : Types.texp}
169

170
171
172
173
   (*a scope contains one of the bindings above and some additional
   information that make substitution and join cheaper*)
   structure Scope : sig
      type scope
Axel Simon's avatar
Axel Simon committed
174
175
176
177
178
179
180
181
      type constraints
      val getFlow : constraints -> BooleanDomain.bfun
      val setFlow : BooleanDomain.bfun -> constraints -> constraints
      val getSize : constraints -> SC.size_constraint_set
      val setSize : SC.size_constraint_set -> constraints -> constraints
      val getCtxt : constraints -> VarInfo.symid list
      val setCtxt : VarInfo.symid list -> constraints -> constraints

182
      type environment = scope list * constraints
Axel Simon's avatar
Axel Simon committed
183
184
      val initial : binding * SC.size_constraint_set -> environment
      val wrap : binding * environment -> environment
185
      val unwrap : environment -> (binding * environment)
Axel Simon's avatar
Axel Simon committed
186
187
      val unwrapDifferent : environment * environment ->
            (binding * binding) option * environment * environment
Axel Simon's avatar
Axel Simon committed
188
      val getVars : environment -> TVar.set
189
      val getBVars : environment -> BD.bvarset
Axel Simon's avatar
Axel Simon committed
190
      val getBVarsUses : ST.symid * BD.bvarset * environment -> BD.bvarset
191
      val getMonoBVars : environment -> BD.bvarset
Axel Simon's avatar
Axel Simon committed
192
      val lookup : ST.symid * environment -> TVar.set * bind_info
193
      val update : ST.symid  *
194
                   (bind_info * constraints -> bind_info * constraints) *
195
                   environment-> environment
Axel Simon's avatar
Axel Simon committed
196
      val toString : scope * TVar.varmap -> string * TVar.varmap
197
198
199
200
   end = struct
      type scope = {
         bindInfo : binding,
         typeVars : TVar.set,
201
         boolVars : BD.bvarset,
202
203
         version : int
      }
Axel Simon's avatar
Axel Simon committed
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
      type constraints = {
         flowInfo : BD.bfun,
         sizeInfo : SC.size_constraint_set,
         context : VarInfo.symid list
      }
      
      fun getFlow { flowInfo = fi, sizeInfo, context } = fi
      fun setFlow fi { flowInfo = _, sizeInfo = si, context = ctxt } =
         { flowInfo = fi, sizeInfo = si, context = ctxt }
      fun getSize { flowInfo, sizeInfo = si, context } = si
      fun setSize si { flowInfo = fi, sizeInfo = _, context = ctxt } =
         { flowInfo = fi, sizeInfo = si, context = ctxt }
      fun getCtxt { flowInfo, sizeInfo, context = ctxt } = ctxt
      fun setCtxt ctxt { flowInfo = fi, sizeInfo = si, context = _ } =
         { flowInfo = fi, sizeInfo = si, context = ctxt }

220
      type environment = scope list * constraints
Axel Simon's avatar
Axel Simon committed
221
   
Axel Simon's avatar
Axel Simon committed
222
      val verCounter = ref 1
223
224
225
226
227
228
      fun nextVersion () =  let
           val v = !verCounter
         in
           (verCounter := v+1; v)
         end             

229
230
231
232
233
      fun isContextRelevant (ctxt1, ctxt2) =
         List.foldl (fn (sym, hasCommon) => hasCommon orelse
                     List.exists (fn sym' => ST.eq_symid (sym',sym)) ctxt2)
                    false ctxt1

Axel Simon's avatar
Axel Simon committed
234
      fun prevTVars [] = TVar.empty
Axel Simon's avatar
Axel Simon committed
235
        | prevTVars ({bindInfo, typeVars = tv, boolVars, version}::_) = tv
236

237
238
239
      fun varsOfBinding (KAPPA {ty=t}, set) = texpVarset (t,set)
        | varsOfBinding (SINGLE {name, ty=t}, set) = texpVarset (t,set)
        | varsOfBinding (GROUP bs, set) = let
240
241
           fun vsOpt (SOME t,set) = texpVarset (t,set)
             | vsOpt (NONE,set) = set
242
243
           fun bvsOpt (SOME (t,_),set) = texpVarset (t,set)
             | bvsOpt (NONE,set) = set
244
245
246
           fun getUsesVars ((ctxt',t),set) = texpVarset (t,set)
           fun getBindVars ({name=n, ty=t, width=w, uses},set) =
               List.foldl getUsesVars
247
                  (bvsOpt (t, vsOpt (w,set)))
Axel Simon's avatar
Axel Simon committed
248
                  (SpanMap.listItems uses)
249
250
251
        in
           List.foldl getBindVars set bs
        end
252
      
253
      fun prevBVars [] = BD.emptySet
Axel Simon's avatar
Axel Simon committed
254
        | prevBVars ({bindInfo, typeVars, boolVars = bv, version}::_) = bv
255
256

      val texpBVarset = texpBVarset (fn ((_,v),vs) => BD.addToSet (v,vs))
Axel Simon's avatar
Axel Simon committed
257

258
259
260
      fun bvarsOfBinding (KAPPA {ty}, ctxt, set) = texpBVarset (ty,set)
        | bvarsOfBinding (SINGLE {name, ty}, ctxt, set) = texpBVarset (ty,set)
        | bvarsOfBinding (GROUP bs, ctxt, set) =
Axel Simon's avatar
Axel Simon committed
261
         let
262
263
            fun getUsesVars ((ctxt',t),set) =
               if isContextRelevant (ctxt',ctxt) then
Axel Simon's avatar
Axel Simon committed
264
265
266
                  texpBVarset (t,set)
               else
                  set
267
268
            fun getBindVars ({name=n, ty=tOpt, width, uses},set) =
               List.foldl getUsesVars
269
270
                  (if List.exists (fn sym => ST.eq_symid (sym,n)) ctxt
                   then case tOpt of
271
272
273
                     NONE => set | SOME (t,_) => texpBVarset (t,set)
                   else set)
                  (SpanMap.listItems uses)
Axel Simon's avatar
Axel Simon committed
274
275
276
277

         in
            List.foldl getBindVars set bs
         end
278

Axel Simon's avatar
Axel Simon committed
279
      fun initial (b, scs) =
280
281
         ([{
            bindInfo = b,
282
            typeVars = varsOfBinding (b, TVar.empty),
Axel Simon's avatar
Axel Simon committed
283
            boolVars = BD.emptySet,
284
            version = 0
Axel Simon's avatar
Axel Simon committed
285
286
287
288
289
290
          }], {
            flowInfo = BD.empty,
            sizeInfo = scs,
            context = []
          })
      fun wrap (b, (scs, state)) =
291
292
         ({
            bindInfo = b,
293
294
            typeVars = varsOfBinding (b, prevTVars scs),
            boolVars = bvarsOfBinding (b, getCtxt state, prevBVars scs),
295
            version = nextVersion ()
Axel Simon's avatar
Axel Simon committed
296
297
298
299
         }::scs,state)
      fun unwrap ({bindInfo = bi, typeVars, boolVars, version} :: scs, state) =
            (bi, (scs, state))
        | unwrap ([], state) = raise InferenceBug
Axel Simon's avatar
Axel Simon committed
300
      fun unwrapDifferent
Axel Simon's avatar
Axel Simon committed
301
            ((all1 as ({bindInfo = bi1, typeVars = _, boolVars = _, version = v1 : int}::scs1,
302
             cons1))
Axel Simon's avatar
Axel Simon committed
303
            ,(all2 as ({bindInfo = bi2, typeVars = _, boolVars = _, version = v2 : int}::scs2,
304
             cons2))) =
Axel Simon's avatar
Axel Simon committed
305
            if v1=v2 then (NONE, all1, all2)
306
            else (SOME (bi1,bi2),(scs1,cons1),(scs2,cons2))
Axel Simon's avatar
Axel Simon committed
307
308
309
        | unwrapDifferent (all1 as ([], _), all2 as ([], _)) =
            (NONE, all1, all2)
        | unwrapDifferent (_, _) = raise InferenceBug
310
      
311
      fun getVars (scs, state) = prevTVars scs
Axel Simon's avatar
Axel Simon committed
312

313
      fun getBVars (scs, state) = prevBVars scs
314

Axel Simon's avatar
Axel Simon committed
315
316
317
318
      fun getBVarsUses (sym, vs, (scs,_)) =
         let
            fun getUsesVars ((ctxt,t),set) =
               if List.exists (fn x => ST.eq_symid (sym,x)) ctxt then
319
                  texpBVarset (t,set)
Axel Simon's avatar
Axel Simon committed
320
321
322
323
               else
                  set
            fun getBindVars ({name, ty, width, uses},set) =
               List.foldl getUsesVars set (SpanMap.listItems uses)
Axel Simon's avatar
Axel Simon committed
324
            fun getGroupVars ({bindInfo = bi, typeVars, boolVars, version},set) =
Axel Simon's avatar
Axel Simon committed
325
326
327
328
329
330
331
               case bi of
                    KAPPA {ty} => set
                  | SINGLE {name, ty} => set
                  | GROUP bs => List.foldl getBindVars set bs
         in
            List.foldl getGroupVars vs scs
         end
332
333

      fun getMonoBVars (bis,_) = List.foldl
Axel Simon's avatar
Axel Simon committed
334
        (fn ({bindInfo = bi, typeVars, boolVars, version},set) => 
335
         case bi of
336
337
              KAPPA { ty = t } => texpBVarset (t,set)
            | SINGLE { ty = t,... } => texpBVarset (t,set)
338
339
            | GROUP _ => set)
        BD.emptySet bis
340

341
      fun lookup (sym, (scs, cons)) =
342
         let
Axel Simon's avatar
Axel Simon committed
343
344
            fun l [] = (TextIO.print ("urk, tried to lookup non-exitent symbol " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")
                       ;raise InferenceBug)
Axel Simon's avatar
Axel Simon committed
345
346
              | l ({bindInfo = KAPPA _, typeVars, boolVars, version}::scs) = l scs
              | l ({bindInfo = SINGLE {name, ty}, typeVars, boolVars, version}::scs) =
Axel Simon's avatar
Axel Simon committed
347
                  if ST.eq_symid (sym,name) then
348
                     (prevTVars scs, SIMPLE { ty = ty})
Axel Simon's avatar
Axel Simon committed
349
                  else l scs
Axel Simon's avatar
Axel Simon committed
350
              | l ({bindInfo = GROUP bs, typeVars, boolVars, version}::scs) =
Axel Simon's avatar
Axel Simon committed
351
352
                  let fun lG other [] = l scs
                        | lG other ((b as {name, ty, width, uses})::bs) =
353
                           if ST.eq_symid (sym,name) then
354
                              (varsOfBinding (GROUP (other @ bs), prevTVars scs),
Axel Simon's avatar
Axel Simon committed
355
                              COMPOUND { ty = ty, width = width, uses = uses })
Axel Simon's avatar
Axel Simon committed
356
                           else lG (b :: other) bs
357
                  in
Axel Simon's avatar
Axel Simon committed
358
                     lG [] bs
359
360
361
362
                  end
         in
            l scs
         end
Axel Simon's avatar
Axel Simon committed
363

364
365
      fun update (sym, action, env) =
         let
366
367
            fun tryUpdate (KAPPA _, cons) = NONE
              | tryUpdate (SINGLE {name, ty}, cons) =
368
369
                if ST.eq_symid (sym,name) then
                  let
370
                     val (SIMPLE {ty}, cons) = action (SIMPLE {ty = ty}, cons)
371
                  in
372
                     SOME (SINGLE {name = name, ty = ty}, cons)
373
374
                  end
                else NONE
375
              | tryUpdate (GROUP bs, cons) =
376
377
378
379
               let fun upd (otherBs, []) = NONE
                     | upd (otherBs, (b as {name, ty, width, uses})::bs) =
                        if ST.eq_symid (sym,name) then
                           let val (COMPOUND { ty = ty, width = width,
380
                                               uses = uses }, cons) =
381
                                   action (COMPOUND { ty = ty, width = width,
382
                                                      uses = uses }, cons)
383
384
385
386
                           in
                              SOME (GROUP (List.revAppend (otherBs,
                                          {name = name, ty = ty,
                                          width = width, uses = uses} :: bs))
387
                                   ,cons)
388
389
390
391
392
393
                           end
                        else upd (b::otherBs, bs)
               in
                  upd ([],bs)
               end
            fun unravel (bs, env) = case unwrap env of
394
395
               (b, env as (scs, cons)) =>
                  (case tryUpdate (b, cons) of
396
                       NONE => unravel (b::bs, env)
397
                     | SOME (b,cons) => List.foldl wrap (scs, cons) (b::bs) )
398
399
400
         in
            unravel ([], env)
         end
Axel Simon's avatar
Axel Simon committed
401
      fun showVarsVer (typeVars,boolVars,ver,si) =
Axel Simon's avatar
Axel Simon committed
402
403
         let
            val (vsStr, si) = TVar.setToString (typeVars,si)
404
            val bsStr = BD.setToString boolVars
Axel Simon's avatar
Axel Simon committed
405
         in
Axel Simon's avatar
Axel Simon committed
406
            (", ver=" ^ Int.toString(ver) ^
Axel Simon's avatar
Axel Simon committed
407
             (*", bvars = " ^ bsStr ^ *) ", vars=" ^ vsStr, si)
Axel Simon's avatar
Axel Simon committed
408
409
         end

Axel Simon's avatar
Axel Simon committed
410
      fun toString ({bindInfo = KAPPA {ty}, typeVars, boolVars, version}, si) =
Axel Simon's avatar
Axel Simon committed
411
            let
Axel Simon's avatar
Axel Simon committed
412
               val (scStr, si) = showVarsVer (typeVars, boolVars, version, si)
Axel Simon's avatar
Axel Simon committed
413
414
415
416
               val (tStr, si) = showTypeSI (ty,si)
            in
               ("KAPPA : " ^ tStr ^ scStr, si)
            end
Axel Simon's avatar
Axel Simon committed
417
        | toString ({bindInfo = SINGLE {name, ty}, typeVars, boolVars, version}, si) =
Axel Simon's avatar
Axel Simon committed
418
            let
Axel Simon's avatar
Axel Simon committed
419
               val (scStr, si) = showVarsVer (typeVars, boolVars, version, si)
Axel Simon's avatar
Axel Simon committed
420
421
               val (tStr, si) = showTypeSI (ty,si)
            in
422
               ("SYMBOL " ^ ST.getString(!SymbolTables.varTable, name) ^
Axel Simon's avatar
Axel Simon committed
423
424
                " : " ^ tStr ^ scStr, si)
            end
Axel Simon's avatar
Axel Simon committed
425
        | toString ({bindInfo = GROUP bs, typeVars, boolVars, version}, si) =
Axel Simon's avatar
Axel Simon committed
426
            let
Axel Simon's avatar
Axel Simon committed
427
               val (scStr, si) = showVarsVer (typeVars, boolVars, version, si)
Axel Simon's avatar
Axel Simon committed
428
429
430
431
432
433
               fun prTyOpt (NONE, str, si) = ("", si)
                 | prTyOpt (SOME t, str, si) = let
                    val (tStr, si) = showTypeSI (t, si)
                 in
                     (str ^ tStr, si)
                 end
434
435
436
437
438
439
               fun prBTyOpt (NONE, str, si) = ("", si)
                 | prBTyOpt (SOME (t,bFun), str, si) = let
                    val (tStr, si) = showTypeSI (t, si)
                 in
                     (str ^ tStr ^ ", flow:" ^ BD.showBFun bFun, si)
                 end
mb0's avatar
mb0 committed
440
               fun printU (({span=(p1,p2),file=_}, (ctxt, t)), (str, sep, si)) =
Axel Simon's avatar
Axel Simon committed
441
442
                  let
                     val (tStr, si) = showTypeSI (t, si)
Axel Simon's avatar
Axel Simon committed
443
444
                     fun showSym (s,(sep,str)) = (",", str ^ sep ^
                           ST.getString(!SymbolTables.varTable, s))
Axel Simon's avatar
Axel Simon committed
445
446
447
448
                  in
                     (str ^
                      sep ^ Int.toString(Position.toInt p1) ^
                      "-" ^ Int.toString(Position.toInt p2) ^
Axel Simon's avatar
Axel Simon committed
449
                      "@" ^ #2 (List.foldl showSym ("","") ctxt) ^
Axel Simon's avatar
Axel Simon committed
450
                      ":" ^ tStr
Axel Simon's avatar
Axel Simon committed
451
                     ,"\n\tuse at ", si)
Axel Simon's avatar
Axel Simon committed
452
453
454
                  end
               fun printB ({name,ty,width,uses}, (str, si)) =
                  let
455
                     val (tStr, si) = prBTyOpt (ty, " : ", si)
Axel Simon's avatar
Axel Simon committed
456
457
                     val (wStr, si) = prTyOpt (width, ", width = ", si)
                     val (uStr, _, si) = 
Axel Simon's avatar
Axel Simon committed
458
                           List.foldl printU ("", "\n\tuse at ", si)
Axel Simon's avatar
Axel Simon committed
459
                                      (SpanMap.listItemsi uses)
Axel Simon's avatar
Axel Simon committed
460
461
462
463
464
465
466
467
                  in
                    (str ^
                     "\n  " ^ ST.getString(!SymbolTables.varTable, name) ^
                     tStr ^ wStr ^ uStr
                    ,si)
                  end
                val (bsStr, si) = List.foldr printB ("", si) bs
            in
468
               ("GROUP" ^ scStr ^ bsStr, si)
Axel Simon's avatar
Axel Simon committed
469
470
            end
               
471
   end
Axel Simon's avatar
Axel Simon committed
472
   
473
   type environment = Scope.environment
Axel Simon's avatar
Axel Simon committed
474

Axel Simon's avatar
Axel Simon committed
475
   fun primitiveEnvironment (l,scs) = Scope.initial
476
477
478
      (GROUP (List.map (fn (s,t,bFunGen,ow) =>
         {name = s, ty = SOME (t,bFunGen BD.empty),
          width = ow, uses = SpanMap.empty}) l),
Axel Simon's avatar
Axel Simon committed
479
       scs)
480
481
482
   
   fun pushSingle (sym, t, env) = Scope.wrap (SINGLE {name = sym, ty = t},env)
   
Axel Simon's avatar
Axel Simon committed
483
   structure SymbolSet = RedBlackSetFn (
Axel Simon's avatar
Axel Simon committed
484
485
486
      struct
         type ord_key = SymbolTable.symid
         val compare = SymbolTable.compare_symid
Axel Simon's avatar
Axel Simon committed
487
488
      end)
          
489
   fun pushGroup (syms, env) = 
Axel Simon's avatar
Axel Simon committed
490
491
492
      let
         val (funs, nonFuns) = List.partition (fn (s,dec) => not dec) syms
         val funDefs = List.map
Axel Simon's avatar
Axel Simon committed
493
            (fn (s,_) => {name = s, ty = NONE, width = NONE, uses = SpanMap.empty})
Axel Simon's avatar
Axel Simon committed
494
            funs
Axel Simon's avatar
Axel Simon committed
495
         val nonFunSyms =
Axel Simon's avatar
Axel Simon committed
496
            SymbolSet.listItems (SymbolSet.fromList (List.map (fn (s,_) => s) nonFuns))
Axel Simon's avatar
Axel Simon committed
497
498
499
         val nonFunDefs = List.map
            (fn s => {name = s, ty = NONE, width =
              SOME (VAR (TVar.freshTVar (), BD.freshBVar ())),
Axel Simon's avatar
Axel Simon committed
500
              uses = SpanMap.empty}) nonFunSyms
Axel Simon's avatar
Axel Simon committed
501
      in                                                                    
502
         Scope.wrap (GROUP (funDefs @ nonFunDefs), env)
Axel Simon's avatar
Axel Simon committed
503
504
      end                                    

505
506
507
   fun popGroup (env, true) = (case Scope.unwrap env of
        (KAPPA {ty=t}, env) =>
         let
Axel Simon's avatar
Axel Simon committed
508
           val (badUses, env) = popGroup (env, false)
509
         in
Axel Simon's avatar
Axel Simon committed
510
            (badUses, Scope.wrap (KAPPA {ty=t}, env))
511
512
513
         end
       | _ => raise InferenceBug)
     | popGroup (env, false) = case Scope.unwrap env of
514
        (GROUP bs, env) =>
Axel Simon's avatar
Axel Simon committed
515
516
         let
            val remVars = Scope.getVars env
Axel Simon's avatar
Axel Simon committed
517
            val (scs, state) = env
518
519
            (*figure out if there are any function usages that have unresolved
            type variables that relate to sizes*)
Axel Simon's avatar
Axel Simon committed
520
            val curVars = SC.getVarset (Scope.getSize state)
Axel Simon's avatar
Axel Simon committed
521
            val unbounded = TVar.difference (curVars,remVars)
522
            (*val _ = TextIO.print ("unbounded vars: " ^ #1 (TVar.setToString (unbounded,TVar.emptyShowInfo)) ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
523
            val siRef = ref TVar.emptyShowInfo
Axel Simon's avatar
Axel Simon committed
524
            fun showUse (n, (ctxt,t)) =
Axel Simon's avatar
Axel Simon committed
525
526
527
528
               let
                  val nStr = SymbolTable.getString(!SymbolTables.varTable, n)
                  val (tStr, si) = showTypeSI (t, !siRef)
                  val vs = texpVarset (t,TVar.empty)
Axel Simon's avatar
Axel Simon committed
529
                  val (cStr, si) = SC.toStringSI (Scope.getSize state, SOME vs, si)
Axel Simon's avatar
Axel Simon committed
530
531
532
533
534
               in
                  (siRef := si
                  ; nStr ^ " : " ^ tStr ^ " has ambiguous vector sizes" ^
                     (if String.size cStr=0 then "" else " where " ^ cStr))
               end
535
            val unbounded = List.foldl (fn
536
                  ({name,ty=SOME (t,_),width,uses},vs) =>
537
                     TVar.difference (vs, texpVarset (t,TVar.empty))
538
                  | (_,vs) => vs)
539
                  unbounded bs
Axel Simon's avatar
Axel Simon committed
540
541
542
543
            val badSizes = List.concat (
               List.map (fn {name = n,ty,width,uses = us} =>
                  List.map (fn (sp,t) => (sp, showUse (n, t))) (
                     SpanMap.listItemsi (
Axel Simon's avatar
Axel Simon committed
544
                        SpanMap.filter (fn (_,t) =>
Axel Simon's avatar
Axel Simon committed
545
546
547
                           not (TVar.isEmpty (TVar.intersection
                              (texpVarset (t,TVar.empty), unbounded)))
                           ) us))) bs)
548
549
            (*project out variables from the size and Boolean domains that are
            no longer needed*)
Axel Simon's avatar
Axel Simon committed
550
            val sCons = SC.filter (remVars, Scope.getSize state)
Axel Simon's avatar
Axel Simon committed
551
         in
Axel Simon's avatar
Axel Simon committed
552
            (badSizes, (scs, Scope.setSize sCons state))
Axel Simon's avatar
Axel Simon committed
553
         end
554
555
      | _ => raise InferenceBug

556
   fun pushTop env = 
Axel Simon's avatar
Axel Simon committed
557
558
559
560
      let
         val a = TVar.freshTVar ()
         val b = BD.freshBVar ()
      in
561
         Scope.wrap (KAPPA {ty = VAR (a,b)}, env)
Axel Simon's avatar
Axel Simon committed
562
      end
563

Axel Simon's avatar
Axel Simon committed
564
   fun pushType (true, t, (scs, state)) =
Axel Simon's avatar
Axel Simon committed
565
      let
Axel Simon's avatar
Axel Simon committed
566
567
568
         val (t,bFun,sCons) = instantiateType (TVar.empty,t,TVar.empty,
                                               Scope.getFlow state,
                                               Scope.getSize state)
Axel Simon's avatar
Axel Simon committed
569
      in
Axel Simon's avatar
Axel Simon committed
570
571
         (Scope.wrap (KAPPA {ty = t}, (scs, Scope.setSize sCons (
                                             Scope.setFlow bFun state))))
Axel Simon's avatar
Axel Simon committed
572
      end
573
     | pushType (false, t, env) = Scope.wrap (KAPPA {ty = t}, env)
Axel Simon's avatar
Axel Simon committed
574

Axel Simon's avatar
Axel Simon committed
575
   fun pushMonadType (t, (scs, state)) =
576
577
578
579
580
581
      let
         val tvar = TVar.freshTVar ()
         val fromBVar = BD.freshBVar ()
         val toBVar = BD.freshBVar ()
         val fromVar = VAR (tvar, fromBVar)
         val toVar = VAR (tvar, toBVar)
Axel Simon's avatar
Axel Simon committed
582
583
584
585
586
         val bFun = BD.meetVarImpliesVar (fromBVar, toBVar) (Scope.getFlow state)
         val (t,bFun,sCons) = instantiateType (texpVarset(t,TVar.empty),t,
                                               TVar.empty,
                                               bFun,
                                               Scope.getSize state)
587
      in
Axel Simon's avatar
Axel Simon committed
588
589
         Scope.wrap (KAPPA {ty = MONAD (t, fromVar, toVar)},
                     (scs, Scope.setSize sCons (Scope.setFlow bFun state)))
590
591
      end

Axel Simon's avatar
Axel Simon committed
592
593
594
595
596
597
598
599
600
   fun pushWidth (sym, env) =
      (case Scope.lookup (sym,env) of
          (_, COMPOUND {ty, width = SOME t, uses}) =>
            Scope.wrap (KAPPA {ty = t}, env)
        | _ => raise (UnificationFailure (
            SymbolTable.getString(!SymbolTables.varTable, sym) ^
            " is not a decoder"))
      )

Axel Simon's avatar
Axel Simon committed
601
602
603
   exception LookupNeedsToAddUse

   fun eq_span ((p1s,p1e), (p2s,p2e)) =
604
605
606
      Position.toInt p1s=Position.toInt p2s andalso
      Position.toInt p1e=Position.toInt p2e

Axel Simon's avatar
Axel Simon committed
607
   fun toStringSI ((scs, state),si) = 
608
      let
609
         fun showCons (s, (str, si)) =
610
611
612
613
614
            let
               val (bStr, si) = Scope.toString (s, si)
            in
               (bStr ^ "\n" ^ str, si)
            end
Axel Simon's avatar
Axel Simon committed
615
         val (sStr, si) = SC.toStringSI (Scope.getSize state, NONE, si)
616
617
         val (envConsStr, si) =
            List.foldr showCons ("sizes: " ^ sStr ^ "\n", si) scs
Axel Simon's avatar
Axel Simon committed
618
619
620
         fun showCtxt [] = "top level"
           | showCtxt [f] = ST.getString(!SymbolTables.varTable, f)
           | showCtxt (f::fs) = showCtxt [f] ^ ";" ^ showCtxt fs
621
      in
Axel Simon's avatar
Axel Simon committed
622
623
         ("environment at " ^ showCtxt (Scope.getCtxt state) ^ "\n" ^
          envConsStr ^ BD.showBFun (Scope.getFlow state) ^ "\n", si)
624
625
      end

626
627
628
629
630
631
632
   fun toString env =
      let
         val (str, _) = toStringSI (env,TVar.emptyShowInfo)
      in
         str
      end
   
633
   fun topToStringSI (env, si) =
Axel Simon's avatar
Axel Simon committed
634
      let
Axel Simon's avatar
Axel Simon committed
635
636
637
         fun tts acc (sc :: scs, state) =
            (case Scope.unwrap (sc :: scs, state) of
                 (GROUP _, (_, state)) => toStringSI ((acc @ [sc], state), si)
Axel Simon's avatar
Axel Simon committed
638
               | (_, env) => tts (acc @ [sc]) env) 
Axel Simon's avatar
Axel Simon committed
639
           | tts acc ([], state) = toStringSI ((acc, state), si)
Axel Simon's avatar
Axel Simon committed
640
641
642
      in
         tts [] env
      end
643

644
645
646
647
648
649
650
   fun topToString env =
      let
         val (str, _) = topToStringSI (env,TVar.emptyShowInfo)
      in
         str
      end

Axel Simon's avatar
Axel Simon committed
651
   fun kappaToStringSI (env, si) = (case Scope.unwrap env of
Axel Simon's avatar
Axel Simon committed
652
653
654
655
656
657
        (KAPPA {ty = t}, _) =>
         let
            val (tStr, si) = showTypeSI (t,si)
         in
            (tStr ^ "\n", si)
         end
Axel Simon's avatar
Axel Simon committed
658
659
      | _ => raise InferenceBug
   )
660

661
   fun funTypeToStringSI (env, f, si) = (case Scope.lookup (f,env) of
662
        (_, COMPOUND { ty = SOME (t,_), width, uses }) => showTypeSI (t,si)
663
664
      | _ => raise InferenceBug
   )
665

666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
   fun reduceBooleanFormula (sym,t,setType,reduceToMono,env) =
      let
         (*we need to restrict the size of the Boolean formula in two
         ways: first, for the function we need all Boolean variables
         in its type, all lambda- and kappa-bound types in the
         environment as well as all the uses of other functions that
         occur in it; secondly, the analysis must continue with a
         Boolean formula that contians the Boolean variables of all
         lambda- and kappa-bound types in the environment. Since the
         latter is usually an empty environment (namely for all
         top-level functions), we first calculate the set of Boolean
         variables in kappa- and lambda-bound types and use that for
         the Boolean formula of the function; then we project onto
         the variables in kappa- and lambda-bound types*)
         val monoBVars = Scope.getMonoBVars env
         val funBVars = Scope.getBVarsUses (sym, monoBVars, env)
         val funBVars = texpBVarset (fn ((_,v),vs) => BD.addToSet (v,vs)) (t, funBVars)
Axel Simon's avatar
Axel Simon committed
683
684
         val (scs, state) = env
         val bFun = BD.projectOnto (funBVars,Scope.getFlow state)
685
686
687
         val bFunRem = if reduceToMono then BD.projectOnto (monoBVars,bFun)
                       else bFun
         val state = Scope.setFlow bFunRem state
Axel Simon's avatar
Axel Simon committed
688
         val env = Scope.update (sym, setType (t,bFun), (scs, state))
689
690
691
692
      in
         env
      end

Axel Simon's avatar
Axel Simon committed
693
694
   fun affectedFunctions (substs, env) =
      let
695
696
697
698
699
700
701
         fun aF (ss, substs, ([], _)) = ss
           | aF (ss, substs, env) = if isEmpty substs then ss else
             case Scope.unwrap env of
              (KAPPA {ty}, env) =>
              aF (ss, substsFilter (substs, Scope.getVars env), env)
            | (SINGLE {name = n, ty = t}, env) =>
              aF (ss, substsFilter (substs, Scope.getVars env), env)
Axel Simon's avatar
Axel Simon committed
702
703
            | (GROUP l, env) =>
            let
704
705
               fun aFL (ss, []) =
                   aF (ss, substsFilter (substs, Scope.getVars env), env)
Axel Simon's avatar
Axel Simon committed
706
                 | aFL (ss, {name, ty = NONE, width, uses} :: l) = aFL (ss, l)
707
                 | aFL (ss, {name = n, ty = SOME (t,_), width, uses} :: l) =
Axel Simon's avatar
Axel Simon committed
708
709
710
711
712
713
714
715
                     if isEmpty (substsFilter (substs,
                        texpVarset (t,TVar.empty)))
                     then aFL (ss, l)
                     else aFL (SymbolSet.add' (n, ss), l)
            in
               aFL (ss, l)
            end
      in
716
         aF (SymbolSet.empty, substs, env)
Axel Simon's avatar
Axel Simon committed
717
718
      end

719
720
721
   fun affectedField (bVar, env) =
      let
         fun aF (_, SOME f) = SOME f
Axel Simon's avatar
Axel Simon committed
722
           | aF (([],_), NONE) = NONE
723
724
725
726
727
           | aF (env, NONE) = case Scope.unwrap env of
              (KAPPA {ty = t}, env) => aF (env, fieldOfBVar (bVar, t))
            | (SINGLE {name, ty = t}, env) => aF (env, fieldOfBVar (bVar, t))
            | (GROUP l, env) =>
            let
Axel Simon's avatar
Axel Simon committed
728
729
               fun findField ((_,t), SOME f) = SOME f
                 | findField ((_,t), NONE) = fieldOfBVar (bVar, t)
730
731
732
733
               fun aFL {name, ty = tOpt, width, uses} =
                  List.foldl findField
                     (case tOpt of
                          NONE => NONE
734
                        | SOME (t,_) => fieldOfBVar (bVar, t))
735
736
737
738
739
740
741
742
743
744
                     (SpanMap.listItems uses)
            in
               aF (env, case List.mapPartial aFL l of
                       [] => NONE
                     | (f :: _) => SOME f)
            end
      in
         aF (env, NONE)
      end

Axel Simon's avatar
Axel Simon committed
745
   fun flowError (bVar, fOpt, envs) =
746
      let
Axel Simon's avatar
Axel Simon committed
747
748
749
         val fOpt = List.foldl (fn (env,res) => case res of
                       SOME f => SOME f
                     | NONE => affectedField (bVar, env)) fOpt envs
750
         val fStr = case fOpt of
Axel Simon's avatar
Axel Simon committed
751
                 NONE => "some other field" (*" with var " ^ BD.showVar bVar*)
752
753
754
755
756
757
               | SOME f => "field " ^
                  SymbolTable.getString(!SymbolTables.fieldTable, f)
      in
         raise UnificationFailure (fStr ^ " cannot flow here")
      end

Axel Simon's avatar
Axel Simon committed
758
759
   fun meetBoolean (update, env as (scs, state)) =
         (scs, Scope.setFlow (update (Scope.getFlow state)) state)
Axel Simon's avatar
Axel Simon committed
760
            handle (BD.Unsatisfiable bVar) => flowError (bVar, NONE, [env])
761

Axel Simon's avatar
Axel Simon committed
762
763
   fun meetSizeConstraint (update, (scs, state)) =
      (scs, Scope.setSize (update (Scope.getSize state)) state)
764

765
   fun pushSymbol (sym, span, env) =
766
      (case Scope.lookup (sym,env) of
Axel Simon's avatar
Axel Simon committed
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
          (_, SIMPLE {ty = t}) =>
         let
            val tNew = setFlagsToTop t
            val env = Scope.wrap (KAPPA {ty = tNew}, env)
            val l1 = texpBVarset (op ::) (t, [])
            val l2 = texpBVarset (op ::) (tNew, [])
            fun genImpl ((contra1,f1),(contra2,f2),bf) =
               if contra1<>contra2 then raise InferenceBug else
               if contra1 then
                  BD.meetVarImpliesVar (f2,f1) bf
               else
                  BD.meetVarImpliesVar (f1,f2) bf
         in
            meetBoolean (fn bFun => ListPair.foldlEq genImpl bFun (l2, l1), env)
         end
782
        | (tvs, COMPOUND {ty = SOME (t,bFunFun), width = w, uses}) =>
Axel Simon's avatar
Axel Simon committed
783
         let
Axel Simon's avatar
Axel Simon committed
784
            val (scs,state) = env
785
            val ctxt = Scope.getCtxt state
Axel Simon's avatar
Axel Simon committed
786
            val bFun = BD.meet (bFunFun, Scope.getFlow state)
Axel Simon's avatar
Axel Simon committed
787
788
789
            val decVars = case w of
                 SOME t => texpVarset (t,TVar.empty)
               | NONE => TVar.empty
Axel Simon's avatar
Axel Simon committed
790
791
            val (t,bFun,sCons) = instantiateType (tvs, t, decVars, bFun, Scope.getSize state)
            val env = (scs, Scope.setFlow bFun (Scope.setSize sCons state))
792
            (*we need to record the usage sites of all functions (primitives,
Axel Simon's avatar
Axel Simon committed
793
            really) that have explicit size constraints in order to be able
794
795
            to later generate error messages for ambiguous uses of these
            functions*)
796
            fun action (COMPOUND {ty, width, uses},cons) =
Axel Simon's avatar
Axel Simon committed
797
               (COMPOUND {ty = ty, width = width,
798
                uses = SpanMap.insert (uses, span, (ctxt, t))}, cons)
Axel Simon's avatar
Axel Simon committed
799
              | action _ = raise InferenceBug
800
            val env =
Axel Simon's avatar
Axel Simon committed
801
               if TVar.isEmpty (TVar.intersection (decVars, SC.getVarset (Scope.getSize state)))
802
803
               then env
               else Scope.update (sym, action, env)
Axel Simon's avatar
Axel Simon committed
804
         in
805
            Scope.wrap (KAPPA {ty = t}, env)
Axel Simon's avatar
Axel Simon committed
806
807
         end
        | (_, COMPOUND {ty = NONE, width, uses}) =>
Axel Simon's avatar
Axel Simon committed
808
          (case SpanMap.find (uses, span) of
Axel Simon's avatar
Axel Simon committed
809
               SOME (_,t) => Scope.wrap (KAPPA {ty = t}, env)
810
811
             | NONE =>
             let
812
813
                val res = freshVar ()
                val ctxt = Scope.getCtxt (#2 env)
814
                fun action (COMPOUND {ty, width, uses},cons) =
815
                     (COMPOUND {ty = ty, width = width,
816
                      uses = SpanMap.insert (uses, span, (ctxt,res))}, cons)
817
818
819
820
821
822
823
                  | action _ = raise InferenceBug
                val env = Scope.update (sym, action, env)
             in
                Scope.wrap (KAPPA {ty = res}, env)
             end
          )
      )
Axel Simon's avatar
Axel Simon committed
824

Axel Simon's avatar
Axel Simon committed
825
826
   fun getUsages (sym, env) = (case Scope.lookup (sym, env) of
           (_, SIMPLE {ty}) => []
Axel Simon's avatar
Axel Simon committed
827
         | (_, COMPOUND {ty, width, uses = us}) => SpanMap.listKeys us
Axel Simon's avatar
Axel Simon committed
828
829
         )

Axel Simon's avatar
Axel Simon committed
830
831
832
833
834
835
   fun getContextOfUsage (sym, span, env) = (case Scope.lookup (sym, env) of
           (_, SIMPLE {ty}) => raise InferenceBug
         | (_, COMPOUND {ty, width, uses = us}) => 
           #1 (SpanMap.lookup (us, span))
         )

Axel Simon's avatar
Axel Simon committed
836
   fun pushUsage (sym, span, funList, env) = (case Scope.lookup (sym, env) of
Axel Simon's avatar
Axel Simon committed
837
838
           (_, SIMPLE {ty}) => raise InferenceBug
         | (_, COMPOUND {ty, width, uses = us}) =>
Axel Simon's avatar
Axel Simon committed
839
840
841
842
843
844
845
846
847
848
849
850
851
852
            let
               val (fs, t) = SpanMap.lookup (us, span)
               fun gatherBFun (f,bFun) =
                  case List.find (fn (f',_) => ST.eq_symid (f,f')) funList of
                       SOME (_, VALUE { symFlow = bFun', ... }) =>
                        BD.meet (bFun',bFun)
                     | SOME (_, DECODE { symFlow = bFun', ... }) =>
                        BD.meet (bFun',bFun)
                     | NONE => bFun
               fun addUsageBFun bFun = List.foldl gatherBFun bFun fs
               val env = meetBoolean (addUsageBFun, env)
            in
               Scope.wrap (KAPPA {ty = t}, env)
            end
Axel Simon's avatar
Axel Simon committed
853
         )
Axel Simon's avatar
Axel Simon committed
854

855
856
857
   fun getCtxt (scs, state) = Scope.getCtxt state
   
   fun popToUsage (sym, span, oldCtxt, env) = (case Scope.unwrap env of
Axel Simon's avatar
Axel Simon committed
858
859
        (KAPPA {ty = tUse}, env) =>
         let
860
            val changedFuns = ref ([] : ST.symid list)