inference.sml 34 KB
Newer Older
Axel Simon's avatar
Axel Simon committed
1
2
3
4
5
(**
 * ## Perform Type Inference
 *
 * Returns tables with types of each identifier.
 *)
Axel Simon's avatar
Axel Simon committed
6
structure TypeInference : sig
Axel Simon's avatar
Axel Simon committed
7

8
   type symbol_types = (SymbolTable.symid * Environment.symbol_type) list
Axel Simon's avatar
Axel Simon committed
9
       
Axel Simon's avatar
Axel Simon committed
10
11
   val getBitpatLitLength : SpecAbstractTree.bitpat_lit -> int

12
13
14
15
16
17
   val typeInferencePass: (Error.err_stream * ResolveTypeInfo.type_info * 
                           SpecAbstractTree.specification) -> symbol_types
   val run: ResolveTypeInfo.type_info * SpecAbstractTree.specification ->
            symbol_types CompilationMonad.t
   
   val showTable : symbol_types -> string
Axel Simon's avatar
Axel Simon committed
18
19
   
end = struct
Axel Simon's avatar
Axel Simon committed
20
21
22
23

   structure AST = SpecAbstractTree
   structure E = Environment
   structure BD = BooleanDomain
24
   structure TI = ResolveTypeInfo
Axel Simon's avatar
Axel Simon committed
25
   structure S = Substitutions
Axel Simon's avatar
Axel Simon committed
26
   structure PP = SpecAbstractTree.PP
Axel Simon's avatar
Axel Simon committed
27
   
28
29
   type symbol_types = (SymbolTable.symid * E.symbol_type) list

Axel Simon's avatar
Axel Simon committed
30
   open Types
Axel Simon's avatar
Axel Simon committed
31

Axel Simon's avatar
Axel Simon committed
32
33
34
35
36
   exception TypeError

   infix >>= >>
   
   type rhsInfo = (SymbolTable.symid *
Axel Simon's avatar
Axel Simon committed
37
38
                   (*pattern and guard for decode function*)
                   (AST.decodepat list * AST.exp option) option *
Axel Simon's avatar
Axel Simon committed
39
40
41
                   AST.var_bind list *       (*arguments*)
                   AST.exp)

Axel Simon's avatar
Axel Simon committed
42
43
44
45
46
47
48
49
50
51
   fun showProg (max,pp,p) =
      let
         val str = Layout.tostring (pp p)
         val str = String.translate
                     (fn c => case c of #"\n" => " " | _ => Char.toString c)
                     str
         val len = String.size str
         fun rep n = if n>0 then " " ^ rep (n-1) else ""
      in
         if len<=max then str ^ rep (max-len) else
Axel Simon's avatar
Axel Simon committed
52
         String.substring (str,0,max-3) ^ "..."
Axel Simon's avatar
Axel Simon committed
53
54
      end

55
   fun refineError (str, msg, envStrs) =
Axel Simon's avatar
Axel Simon committed
56
      let
57
58
59
60
         fun genRow ((env,str),(acc,si)) =
            let
               val (eStr,si) = E.kappaToStringSI (env,si)
            in
61
               (acc ^ "\t" ^ str ^ ": " ^ eStr,si)
62
63
64
            end
         val (str, si) = List.foldl
                           genRow
65
                           (str ^ msg ^ "\n", TVar.emptyShowInfo) envStrs
Axel Simon's avatar
Axel Simon committed
66
      in
67
         raise S.UnificationFailure str
Axel Simon's avatar
Axel Simon committed
68
69
      end

Axel Simon's avatar
Axel Simon committed
70
71
72
73
74
75
76
77
78
79
80
81
   fun getBitpatLitLength bp =
      let
         val fields = String.fields (fn c => c= #"|") bp
         fun checkWidth (f,width) =
            if String.size f <> width then
                  raise S.UnificationFailure "bit literals have different lengths"
            else width
      in
         case fields of
            [] => 0
          | (f::fs) => List.foldl checkWidth (String.size f) fs
      end
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
   
   (*convert calls in a decoder pattern into a list of monadic actions*)
   fun decsToSeq e [] = e
     | decsToSeq e ds = AST.SEQexp
         (List.concat (List.map decToSeqDecodepat ds) @ [AST.ACTIONseqexp e])
   and decToSeqDecodepat (AST.MARKdecodepat {tree=t, span=s}) =
         List.map (fn a => AST.MARKseqexp {tree=a, span=s})
            (decToSeqDecodepat t)
     | decToSeqDecodepat (AST.TOKENdecodepat tp) =
         List.map AST.ACTIONseqexp (decToSeqToken tp)
     | decToSeqDecodepat (AST.BITdecodepat bps) =
         List.map AST.ACTIONseqexp (List.concat (List.map decToSeqBitpat bps))
   and decToSeqToken (AST.MARKtokpat {tree=t, span=s}) =
         List.map (fn e => AST.MARKexp {tree=e, span=s}) (decToSeqToken t)
     | decToSeqToken (AST.NAMEDtokpat sym) = [AST.IDexp sym]
     | decToSeqToken _ = []
   and decToSeqBitpat (AST.MARKbitpat {tree=t, span=s}) =
         List.map (fn e => AST.MARKexp {tree=e, span=s}) (decToSeqBitpat t)
     | decToSeqBitpat (AST.NAMEDbitpat sym) = [AST.IDexp sym]
     | decToSeqBitpat _ = []
    
103
fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
Axel Simon's avatar
Axel Simon committed
104
   val sm = ref ([] : symbol_types)
105
   val { tsynDefs, typeDefs, conParents} = ti
106
107
   val caseExpSymId = SymbolTable.lookup(!SymbolTables.varTable,
                                         Atom.atom Primitives.caseExpression)
Axel Simon's avatar
Axel Simon committed
108
109
   (*val stateSymId = SymbolTable.lookup(!SymbolTables.varTable,
                                       Atom.atom Primitives.globalState)*)
Axel Simon's avatar
Axel Simon committed
110
111
   val granularitySymId = SymbolTable.lookup(!SymbolTables.varTable,
                                             Atom.atom Primitives.granularity)
Axel Simon's avatar
Axel Simon committed
112
   
Axel Simon's avatar
Axel Simon committed
113
114
115
   val bindSymId = SymbolTable.lookup(!SymbolTables.varTable, Atom.atom ">>")
   val bindASymId = SymbolTable.lookup(!SymbolTables.varTable, Atom.atom ">>=")

mb0's avatar
mb0 committed
116
117
   fun reportError conv (_, env) {span=s, tree=t} =
      conv ({span=s},env) t
Axel Simon's avatar
Axel Simon committed
118
      handle (S.UnificationFailure str) =>
119
         (Error.errorAt (errStrm, s, [str]); raise TypeError)
Axel Simon's avatar
Axel Simon committed
120
   val reportBadSizes = List.app (fn (s,str) => Error.errorAt (errStrm, s, [str]))
121
   fun getSpan {span = s} = s
Axel Simon's avatar
Axel Simon committed
122
123
124

   (* define a first traversal that creates a group of all top-level decls *)
   fun topDecl (AST.MARKdecl {span, tree=t}) = topDecl t
125
126
     | topDecl (AST.DECODEdecl dd) = topDecodeDecl dd
     | topDecl (AST.LETRECdecl vd) = topLetrecDecl vd
Axel Simon's avatar
Axel Simon committed
127
     | topDecl _ = []
128
   and topDecodeDecl (v, _, _) = [(v, true)]
129
   and topLetrecDecl (v, _, _) = [(v,false)]
Axel Simon's avatar
Axel Simon committed
130
   
Axel Simon's avatar
Axel Simon committed
131
   (* define a second traversal that is a full inference of the tree *)
132
133
   
   (*local helper function to infer types for a binding group*)
Axel Simon's avatar
Axel Simon committed
134
   val maxIter = 3
135
   fun calcSubset printWarn env =
Axel Simon's avatar
Axel Simon committed
136
      let
137
         fun checkUsage sym (s, unstable) =
Axel Simon's avatar
Axel Simon committed
138
            let
Axel Simon's avatar
Axel Simon committed
139
               val fs = E.getContextOfUsage (sym, s, env)
140
               val oldCtxt = E.getCtxt env
Axel Simon's avatar
Axel Simon committed
141
142
               val env = List.foldl E.pushFunction env fs
               
143
               val envFun = E.pushSymbol (sym, s, env)
144
               (*val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)*)
Axel Simon's avatar
Axel Simon committed
145
               val envCall = E.pushUsage (sym, s, !sm, env)
146
               (*val _ = TextIO.print ("pushed usage:\n" ^ E.topToString envCall)*)
147
148

               (*warn about refinement of the definition due to a call site*)
Axel Simon's avatar
Axel Simon committed
149
               fun raiseWarning (substs, syms) =
Axel Simon's avatar
Axel Simon committed
150
151
                  if E.SymbolSet.isEmpty syms orelse not printWarn then ()
                  else
Axel Simon's avatar
Axel Simon committed
152
153
154
155
                  let
                     val si = TVar.emptyShowInfo
                     val (sSubst, si) = S.showSubstsSI (substs, si)
                     fun showSyms (sym, (res, pre, si)) =
Axel Simon's avatar
Axel Simon committed
156
                        let
Axel Simon's avatar
Axel Simon committed
157
158
                           val sStr = SymbolTable.getString
                              (!SymbolTables.varTable, sym)
159
                           val (sType, si) = E.funTypeToStringSI (env, sym, si)
Axel Simon's avatar
Axel Simon committed
160
                        in
161
                           (res ^ pre ^ sStr ^ " : " ^ sType, "\n\tand call ", si)
Axel Simon's avatar
Axel Simon committed
162
                        end
Axel Simon's avatar
Axel Simon committed
163
                     val (symsStr, _, _) =
164
                        List.foldl showSyms ("","\n\tfor call ", si)
165
                           (E.SymbolSet.listItems syms)
Axel Simon's avatar
Axel Simon committed
166
167
168
169
170
                  in 
                     (Error.warningAt (errStrm, s, [
                     "call to ",
                     SymbolTable.getString(!SymbolTables.varTable, sym),
                     " requires refinement ", sSubst,
171
                     symsStr]))
Axel Simon's avatar
Axel Simon committed
172
                  end
173
               val substs = E.subseteq (envCall, envFun)
Axel Simon's avatar
Axel Simon committed
174
175
176
177
178
179
               val affectedSyms = E.affectedFunctions (substs,env)
               
               (*val (sStr, si) = S.showSubstsSI (substs, TVar.emptyShowInfo)
               val _ = TextIO.print ("subset: subst=:" ^ sStr ^ ", unstable: " ^
                  List.foldl (fn (sym, res) => res ^ ", " ^ SymbolTable.getString
                   (!SymbolTables.varTable, sym)) "" (E.SymbolSet.listItems affectedSyms) ^ "\n")*)
180
181
               val _ = raiseWarning (substs, affectedSyms)
            in
Axel Simon's avatar
Axel Simon committed
182
183
               if E.SymbolSet.isEmpty affectedSyms then unstable else
                  E.SymbolSet.add (unstable, sym)
184
            end
Axel Simon's avatar
Axel Simon committed
185
186
               handle (S.UnificationFailure str) =>
                  E.SymbolSet.add (unstable, sym)
187
188
189
         fun checkUsages (sym, unstable) =
            let
               val usages = E.getUsages (sym, env)
Axel Simon's avatar
Axel Simon committed
190
               (*val _ = TextIO.print ("***** checking subset of " ^ Int.toString (List.length usages) ^ " usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
               val unstable = List.foldl (checkUsage sym) unstable usages
            in
               unstable
            end
      in
         List.foldl checkUsages E.SymbolSet.empty (E.getGroupSyms env)
      end

   fun calcIteration (unstable, env) =
      let
         fun checkUsage sym (s, env) =
            let
               val fs = E.getContextOfUsage (sym, s, env)
               val oldCtxt = E.getCtxt env
               val env = List.foldl E.pushFunction env fs
               
               val envFun = E.pushSymbol (sym, s, env)
               (*val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)*)
               val envCall = E.pushUsage (sym, s, !sm, env)
               (*val _ = TextIO.print ("pushed usage:\n" ^ E.topToString envCall)*)
               (*inform about a unification failure when checking call site
               with definition*)
               fun raiseError str =
                  let
                     val si = TVar.emptyShowInfo
                     val (sFun, si) = E.kappaToStringSI (envFun, si)
                     val (sCall, si) = E.kappaToStringSI (envCall, si)
                  in 
                     (Error.errorAt (errStrm, s, [str,
                     " when checking call to ",
                     SymbolTable.getString(!SymbolTables.varTable, sym),
                     "\n\tcall provides type  " ^ sCall,
                     "\n\tdefinition has type " ^ sFun]))
                  end
               val env = E.meetFlow (envCall, envFun)
Axel Simon's avatar
Axel Simon committed
226
                  handle (S.UnificationFailure str) =>
227
                     (raiseError str; envCall)
228
               val (changed, env) = E.popToUsage (sym, s, oldCtxt, env)
229
230
231
232
233
               val _ = sm := List.foldl
                     (fn (sym,sm) => (sym, E.getFunctionInfo (sym, env)) ::
                        List.filter (fn (s,_) =>
                           not (SymbolTable.eq_symid(s,sym))) sm)
                     (!sm) changed
Axel Simon's avatar
Axel Simon committed
234
            in
235
236
237
238
239
               env
            end
         fun calcUsages (sym, env) =
            let
               val usages = E.getUsages (sym, env)
Axel Simon's avatar
Axel Simon committed
240
               (*val _ = TextIO.print ("***** re-eval of " ^ Int.toString (List.length usages) ^ " usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
241
242
243
               val env = List.foldl (checkUsage sym) env usages
            in
               env
Axel Simon's avatar
Axel Simon committed
244
            end
Axel Simon's avatar
Axel Simon committed
245
      in
246
         List.foldl calcUsages env (E.SymbolSet.listItems unstable)
Axel Simon's avatar
Axel Simon committed
247
248
      end

249
   fun calcFixpoint curIter env =
Axel Simon's avatar
Axel Simon committed
250
         case calcSubset (curIter>0) env of unstable =>
251
         if E.SymbolSet.isEmpty unstable then env else
252
         if curIter<maxIter then
253
            calcFixpoint (curIter+1) (calcIteration (unstable,env))
Axel Simon's avatar
Axel Simon committed
254
         else
Axel Simon's avatar
Axel Simon committed
255
256
257
258
259
260
         let
            val si = TVar.emptyShowInfo
            fun showSyms (sym, (res, pre, si)) =
               let
                  val sStr = SymbolTable.getString
                     (!SymbolTables.varTable, sym)
261
                  val env = E.pushSymbol (sym, SymbolTable.noSpan, env)
Axel Simon's avatar
Axel Simon committed
262
263
264
265
                  val (sType, si) = E.kappaToStringSI (env, si)
               in
                  (res ^ pre ^ sStr ^ " : " ^ sType, ", ", si)
               end
266
            val symIds = E.SymbolSet.listItems unstable
Axel Simon's avatar
Axel Simon committed
267
268
269
270
271
272
273
            val (symsStr, _, _) = List.foldl showSyms ("", "", si) symIds
            val s = case symIds of [] => raise TypeError | (sym :: _) =>
                    SymbolTable.getSpan(!SymbolTables.varTable, sym)
         in 
            (Error.errorAt (errStrm, s, [
            "no typing found for ",
            symsStr,
Axel Simon's avatar
Axel Simon committed
274
            "\tpass --inference-iterations=",
Axel Simon's avatar
Axel Simon committed
275
276
277
278
279
            Int.toString (maxIter+1),
            " to try a little harder"]); env)
         end
   val calcFixpoint = calcFixpoint 0
   
280
   fun infRhs (st,env) (sym, dec, guard, args, rhs) =
Axel Simon's avatar
Axel Simon committed
281
      let
282
         (*val _ = TextIO.print ("checking binding " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
283
284
         fun checkGuard (g,env) =
            let
285
286
287
               val stateVar = VAR (freshTVar (), BD.freshBVar ())
               val monadType = MONAD (VEC (CONST 1), stateVar, stateVar)
               val envRef = E.pushType (false, monadType, env)
Axel Simon's avatar
Axel Simon committed
288
               val envGua = infExp (st, env) g
Axel Simon's avatar
Axel Simon committed
289
               val env = E.meet (envRef, envGua)
290
291
292
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking guards",
293
294
                            [(envRef, "required guard type        "),
                             (envGua, "guard " ^ showProg (20, PP.exp, g))])
Axel Simon's avatar
Axel Simon committed
295
296
297
298
299
            in
               E.popKappa env
            end
         val env = case guard of SOME g => checkGuard (g,env)
                               | NONE => env
Axel Simon's avatar
Axel Simon committed
300
301
302
         fun pushDecoderBindings(d,(n, env)) =
            case infDecodepat sym (st,env) d of (nArgs, env) => (n+nArgs, env)
         val (n,env) = List.foldl pushDecoderBindings (0,env) dec
Axel Simon's avatar
Axel Simon committed
303
         val env = List.foldl E.pushLambdaVar env args
304
         val rhs = decsToSeq rhs dec
Axel Simon's avatar
Axel Simon committed
305
         val env = infExp (st,env) rhs
306
         val env = E.reduceToFunction (env, List.length args)
Axel Simon's avatar
Axel Simon committed
307
         val env = E.return (n,env)
308
         (*val _ = TextIO.print ("after popping args:\n" ^ E.topToString env)*)
Axel Simon's avatar
Axel Simon committed
309
      in
310
         env
Axel Simon's avatar
Axel Simon committed
311
      end
Axel Simon's avatar
Axel Simon committed
312
   and infBinding (st,env) (sym, args, rhs) =
Axel Simon's avatar
Axel Simon committed
313
      let
314
         val env = E.pushFunction (sym,env)
315
         val env = infRhs (st,env) (sym, [], NONE, args, rhs)
Axel Simon's avatar
Axel Simon committed
316
317
318
319
         val env = E.popToFunction (sym, env)
         val fInfo = E.getFunctionInfo (sym, env)
         val _ = sm := (sym, fInfo) :: !sm
      in
320
         env
Axel Simon's avatar
Axel Simon committed
321
      end
322

Axel Simon's avatar
Axel Simon committed
323
   and infDecl stenv (AST.MARKdecl m) = reportError infDecl stenv m
Axel Simon's avatar
Axel Simon committed
324
325
326
     | infDecl (st,env) (AST.GRANULARITYdecl w) =
      let
         val envGra = E.pushWidth (granularitySymId, env)
Axel Simon's avatar
Axel Simon committed
327
         val envInt = E.pushType (false, CONST (IntInf.toInt w), env)
Axel Simon's avatar
Axel Simon committed
328
         val env = E.meet (envGra, envInt)
Axel Simon's avatar
Axel Simon committed
329
330
         val env = E.popKappa env
      in
331
         env
Axel Simon's avatar
Axel Simon committed
332
      end
Axel Simon's avatar
Axel Simon committed
333
     | infDecl stenv (AST.DECODEdecl dd) = infDecodedecl stenv dd
334
335
     | infDecl (st,env) (AST.LETRECdecl (v,l,e)) = infBinding (st,env) (v, l, e)
     | infDecl (st,env) _ = env
336

337
   and infDecodedecl (st,env) (v, l, Sum.INL e) =
Axel Simon's avatar
Axel Simon committed
338
339
340
      let
         val env = E.pushFunctionOrTop (v,env)
         val envRhs = E.popKappa env
341
         val envRhs = infRhs (st,envRhs) (v, l, NONE, [], e)
342
343
         (*val _ = TextIO.print ("**** decoder type:\n" ^ E.topToString env)
         val _ = TextIO.print ("**** decoder rhs:\n" ^ E.topToString envRhs)*)
Axel Simon's avatar
Axel Simon committed
344
         val env = E.meet (env, envRhs)
Axel Simon's avatar
Axel Simon committed
345
         val env = E.popToFunction (v, env)
Axel Simon's avatar
Axel Simon committed
346
         val fInfo = E.getFunctionInfo (v, env)
Axel Simon's avatar
Axel Simon committed
347
348
         val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
                                       not (SymbolTable.eq_symid(s,v))) (!sm)
Axel Simon's avatar
Axel Simon committed
349
      in
350
         env
Axel Simon's avatar
Axel Simon committed
351
      end
352
     | infDecodedecl (st,env) (v, l, Sum.INR el) =
353
      let
Axel Simon's avatar
Axel Simon committed
354
         val env = E.pushFunctionOrTop (v,env)
355
356
357
         val env = List.foldl
            (fn ((guard, rhs), env) => let
               val envRhs = E.popKappa env
358
               val envRhs = infRhs (st,envRhs) (v, l, SOME guard, [], rhs)
Axel Simon's avatar
Axel Simon committed
359
               val env = E.meet (env, envRhs)
360
361
362
            in
               env
            end) env el
Axel Simon's avatar
Axel Simon committed
363
         val env = E.popToFunction (v, env)
Axel Simon's avatar
Axel Simon committed
364
         val fInfo = E.getFunctionInfo (v, env)
Axel Simon's avatar
Axel Simon committed
365
366
         val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
                                       not (SymbolTable.eq_symid(s,v))) (!sm)
367
      in
368
         env
369
      end
370

371
   and infExp stenv (AST.MARKexp m) = reportError infExp stenv m
372
     | infExp (st,env) (AST.LETRECexp (l,e)) =
Axel Simon's avatar
Axel Simon committed
373
      let                                              
374
         val names = List.map topLetrecDecl l
Axel Simon's avatar
Axel Simon committed
375
         val env = E.pushGroup (List.concat names, env)
376
377
378
379
         val env = List.foldl (fn ((v,l,e), env) =>
                        infBinding (st, env) (v, l, e)
                     ) env l
         val env = calcFixpoint env
Axel Simon's avatar
Axel Simon committed
380
         val env = infExp (st,env) e
Axel Simon's avatar
Axel Simon committed
381
         val (badSizes, env) = E.popGroup (env, true)
Axel Simon's avatar
Axel Simon committed
382
         val _ = reportBadSizes badSizes
Axel Simon's avatar
Axel Simon committed
383
      in
Axel Simon's avatar
Axel Simon committed
384
         env
Axel Simon's avatar
Axel Simon committed
385
386
387
      end
     | infExp (st,env) (AST.IFexp (e1,e2,e3)) =
      let
388
389
         val envWant = E.pushType (false, VEC (CONST 1), env)
         val envHave = infExp (st,env) e1
Axel Simon's avatar
Axel Simon committed
390
         val env = E.meet (envWant, envHave)
391
         val env = E.popKappa env
Axel Simon's avatar
Axel Simon committed
392
         val envT = infExp (st,env) e2
393
         (*val _ = TextIO.print ("**** after if-then:\n" ^ E.topToString envT)*)
Axel Simon's avatar
Axel Simon committed
394
         val envE = infExp (st,env) e3
395
         (*val _ = TextIO.print ("**** after if-else:\n" ^ E.topToString envE)*)
396
         val env = E.meet (envE,envT)
Axel Simon's avatar
Axel Simon committed
397
398
399
      in
         env
      end
400
401
402
403
     | infExp (st,env) (AST.CASEexp (e,l)) =
      let
         val (t,env) = E.pushLambdaVar' (caseExpSymId, env)
         val envExp = infExp (st,env) e
404
         (*val _ = TextIO.print ("**** after case exp:\n" ^ E.toString envExp)*)
405
         val envVar = E.pushType (false, t, env)
406
         (*val _ = TextIO.print ("**** after case dup:\n" ^ E.toString envVar)*)
Axel Simon's avatar
Axel Simon committed
407
         val env = E.meetFlow (envVar, envExp)
408
409
         val env = E.popKappa env
         val envNeutral = E.pushTop env
Axel Simon's avatar
Axel Simon committed
410
         fun genFlow ((p,exp), nEnv) =
411
            let
Axel Simon's avatar
Axel Simon committed
412
               val expEnv = infMatch (st,E.popKappa nEnv) (p,exp)
Axel Simon's avatar
Axel Simon committed
413
               val env = E.meetFlow (nEnv, expEnv)
Axel Simon's avatar
Axel Simon committed
414
                  handle S.UnificationFailure str =>
Axel Simon's avatar
Axel Simon committed
415
416
                     refineError (str,
                                  " while checking right-hand-side of branches",
417
418
                                  [(nEnv, "branches so far               "),
                                   (expEnv, showProg (30, PP.exp, exp))])
419
            in
Axel Simon's avatar
Axel Simon committed
420
               env
421
            end
Axel Simon's avatar
Axel Simon committed
422
         val env = List.foldl genFlow envNeutral l
423
424
425
426
         (*val _ = TextIO.print ("**** all envs:\n" ^ E.toString env)*)
      in
         E.return (1,env)
      end
427
428
429
430
431
432
     | infExp stenv (AST.BINARYexp (e1, binop, e2)) =
      let
         fun infixToExp (AST.MARKinfixop {tree = t, span = s}) =
               AST.MARKexp ({tree = infixToExp t, span = s})
           | infixToExp (AST.OPinfixop opid) = AST.IDexp opid
      in
433
         infExp stenv (AST.APPLYexp (infixToExp binop, [e1, e2]))
434
      end
435
     | infExp (st,env) (AST.APPLYexp (e1,es2)) =
Axel Simon's avatar
Axel Simon committed
436
      let                                      
437
         val envFun = infExp (st,env) e1
438
         val envArg = List.foldl (fn (e2,env) => infExp (st,env) e2) env es2
439
440
         (*val _ = TextIO.print ("**** app func:\n" ^ E.topToString envFun)
         val _ = TextIO.print ("**** app arg:\n" ^ E.topToString envArg)*)
Axel Simon's avatar
Axel Simon committed
441
         val envArgRes = E.pushTop envArg
442
         val envArgRes = E.reduceToFunction (envArgRes, List.length es2)
443
         (*val _ = TextIO.print ("**** app turning arg:\n" ^ E.toString envArgRes)*)
Axel Simon's avatar
Axel Simon committed
444
445
446
447
         (* make the result of the call-site depend on the result of the
         function; the flow expressing that formal parameters depend on actual
         parameters follows from contra-variance*)
         val env = E.meetFlow (envArgRes, envFun)
Axel Simon's avatar
Axel Simon committed
448
            handle S.UnificationFailure str =>
Axel Simon's avatar
Axel Simon committed
449
450
               refineError (str,
                            " while passing",
451
452
453
454
455
                            (#1 (List.foldr
                            (fn (e2,(res,env)) => 
                              ((env, "argument    " ^ showProg (20, PP.exp, e2))::res,
                               E.popKappa env)
                            ) ([], envArg) es2)) @
456
                            [(envFun, "to function " ^ showProg (20, PP.exp, e1))])
Axel Simon's avatar
Axel Simon committed
457
         (*val _ = TextIO.print ("**** app fun,res unified:\n" ^ E.topToString env)*)
Axel Simon's avatar
Axel Simon committed
458
         val env = E.reduceToResult env
459
      in
Axel Simon's avatar
Axel Simon committed
460
         env                                                         
461
462
      end
        
463
464
     | infExp (st,env) (AST.RECORDexp l) =
      let
465
466
         val t = freshVar ()
         val env = E.meetBoolean (BD.meetVarZero (bvar t), env)
467
         val env = E.pushType (false, t, env)
468
469
         fun pushField ((fid,e), (nts, env)) =
            let
470
               val env = infExp (st,env) e
471
               val bVar = BD.freshBVar ()
472
               val env = E.meetBoolean (BD.meetVarOne bVar, env)
473
            in
474
               ((bVar, fid) :: nts, env)
475
476
            end
         val (nts, env) = List.foldl pushField ([], env) l
477
         (*val _ = TextIO.print ("**** rec exp, single fields:\n" ^ E.toString env ^ "\n")*)
478
         val env = E.reduceToRecord (nts, env)
479
         (*val _ = TextIO.print ("**** rec exp, combined:\n" ^ E.toString env ^ "\n")*)
480
481
482
483
484
485
486
      in
         env
      end
         
     | infExp (st,env) (AST.SELECTexp f) =
      let
         val env = E.pushTop env
487
488
         val tf = freshVar ()
         val tf' = newFlow tf
489
490
         val env = E.pushType (false, tf, env)
         val exists = BD.freshBVar ()
Axel Simon's avatar
Axel Simon committed
491
         (*val _ = TextIO.print ("**** before rec reduce:\n" ^ E.toString env ^ "\n")*)
492
         val env = E.reduceToRecord ([(exists, f)], env)
Axel Simon's avatar
Axel Simon committed
493
         val env = E.meetBoolean (BD.meetVarImpliesVar (bvar tf', bvar tf) o
494
                                  BD.meetVarOne exists, env)
Axel Simon's avatar
Axel Simon committed
495
         (*val _ = TextIO.print ("**** after rec reduce:\n" ^ E.toString env ^ "\n")*)
496
         val env = E.pushType (false, tf', env)
497
         val env = E.reduceToFunction (env,1)
498
         (*val _ = TextIO.print ("**** rec selector:\n" ^ E.topToString env ^ "\n")*)
499
500
501
      in
         env
      end
502
     | infExp (st,env) (AST.UPDATEexp fs) =
503
      let
504
         val fieldsVar = freshVar ()
505
506
507
508
509
510
511
512
513
514
515
         val env = E.pushType (false, fieldsVar, env)
         fun pushInpField ((fid,e), (nts, env)) =
            let
               val env = E.pushTop env
               val bVar = BD.freshBVar ()
            in
               ((bVar, fid) :: nts, env)
            end
         val (nts, env) = List.foldl pushInpField ([], env) fs
         val env = E.reduceToRecord (nts, env)

516
517
518
         val fieldsVar' = newFlow fieldsVar
         val env = E.meetBoolean (BD.meetVarImpliesVar (bvar fieldsVar', bvar fieldsVar), env)
         val env = E.pushType (false, fieldsVar', env)
Axel Simon's avatar
Axel Simon committed
519
         fun pushOutField ((fid,eOpt), (nts, env)) =
520
            let
521
               (*val _ = TextIO.print ("**** rec update: pushing field " ^ SymbolTable.getString(!SymbolTables.fieldTable, fid) ^ ".\n")*)
522
               val bVar = BD.freshBVar ()
Axel Simon's avatar
Axel Simon committed
523
524
525
526
527
               val env = case eOpt of
                           SOME e => E.meetBoolean (BD.meetVarOne bVar, 
                                       infExp (st,env) e)
                         | NONE => E.meetBoolean (BD.meetVarZero bVar,
                                       E.pushTop env)
528
            in
529
               ((bVar, fid) :: nts, env)
530
531
532
            end
         val (nts, env) = List.foldl pushOutField ([], env) fs
         val env = E.reduceToRecord (nts, env)
533
         val env = E.reduceToFunction (env,1)
534
         (*val _ = TextIO.print ("**** rec update: function is:\n" ^ E.topToString env ^ "\n")*)
535
536
537
      in
         env
      end
Axel Simon's avatar
Axel Simon committed
538
539
     | infExp stenv (AST.LITexp lit) = infLit stenv lit
     | infExp stenv (AST.SEQexp l) = infSeqexp stenv l
Axel Simon's avatar
Axel Simon committed
540
541
     | infExp (st,env) (AST.IDexp v) =
      let
542
         val env = E.pushSymbol (v, getSpan st, env)
543
         (*val _ = TextIO.print ("**** after pushing symbol " ^ SymbolTable.getString(!SymbolTables.varTable, v) ^ ":\n" ^ E.topToString env)*)
Axel Simon's avatar
Axel Simon committed
544
545
546
      in
         env
      end
547
548
549
550
551
     | infExp (st,env) (AST.CONexp c) =
      let
         val dcon = SymMap.lookup (conParents, c)
         val { tdVars = vs, tdCons = cs } = SymMap.lookup (typeDefs, dcon)
         val tArgOpt = SymMap.lookup (cs, c)
552
553
554
555
         val env =
            case tArgOpt of
                 NONE => E.pushType (true, ALG (dcon, List.map VAR vs), env)
               | SOME t =>
Axel Simon's avatar
Axel Simon committed
556
557
558
559
560
            let
               val (posFlags, negFlags) =
                  fieldBVarsets (t,(BD.emptySet, BD.emptySet))
               val env = E.meetBoolean (BD.meetVarSetOne posFlags o
                                        BD.meetVarSetZero negFlags, env)
561
               val env = E.pushType (true, FUN ([t],ALG (dcon, List.map VAR vs)), env)
Axel Simon's avatar
Axel Simon committed
562
563
564
            in
               env
            end
565
         (*val _ = TextIO.print ("**** looking for " ^ SymbolTable.getString(!SymbolTables.conTable, c) ^ ":\n" ^ E.topToString env)*)
566
      in
567
         env
568
      end
569
570
571
572
573
574
575
     | infExp (st,env) (AST.FNexp (vs, e)) =
      let
         val env = List.foldl E.pushLambdaVar env vs
         val env = infExp (st, env) e
      in
         E.reduceToFunction (env, List.length vs)
      end
576
         
Axel Simon's avatar
Axel Simon committed
577
578
579
580
   and infSeqexp stenv [] = raise
         (S.UnificationFailure "last statement in a sequence may not bind a variable")
     | infSeqexp stenv (AST.MARKseqexp m :: l) =
         reportError (fn stenv => fn e => infSeqexp stenv (e :: l)) stenv m
Axel Simon's avatar
Axel Simon committed
581
582
     | infSeqexp (st,env) [AST.ACTIONseqexp e] = infExp (st,env) e
     | infSeqexp (st,env) (s :: l) =
Axel Simon's avatar
Axel Simon committed
583
      let
Axel Simon's avatar
Axel Simon committed
584
585
586
587
         val (bind, vOpt,e) = case s of
               AST.ACTIONseqexp e => (bindSymId, NONE, e)
             | AST.BINDseqexp (v,e) => (bindASymId, SOME v, e)
             | _ => raise TypeError
588
         val envFun = E.pushSymbol (bind, getSpan st, env)
Axel Simon's avatar
Axel Simon committed
589
590
         val envArg = infExp (st,env) e
         val envArgRes = E.pushTop envArg
591
         val envArgRes = E.reduceToFunction (envArgRes,1)
592
         (*val _ = TextIO.print ("function to unify with bind: " ^ E.topToString envArgRes ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
593
         val env = E.meetFlow (envArgRes, envFun)
Axel Simon's avatar
Axel Simon committed
594
            handle S.UnificationFailure str =>
Axel Simon's avatar
Axel Simon committed
595
596
597
598
599
600
               raise S.UnificationFailure (str ^ " in statement\n\t" ^
                   showProg (20, PP.exp, e) ^ " : " ^
                   #1 (E.kappaToStringSI (envArg, TVar.emptyShowInfo)))
         val envFun = E.reduceToResult env
         val env = E.popKappa envFun
         val envArg = case vOpt of
601
                 SOME v => E.reduceToFunction (infSeqexp (st, E.pushLambdaVar (v,env)) l,1)
Axel Simon's avatar
Axel Simon committed
602
603
               | NONE => infSeqexp (st, env) l
         val envArgRes = E.pushTop envArg
604
         val envArgRes = E.reduceToFunction (envArgRes,1)
Axel Simon's avatar
Axel Simon committed
605
         val env = E.meetFlow (envArgRes, envFun)
Axel Simon's avatar
Axel Simon committed
606
607
            handle S.UnificationFailure str =>
               refineError (str,
Axel Simon's avatar
Axel Simon committed
608
                            " when passing on the result of",
609
610
                            [(envFun, "statement " ^ showProg (20, PP.exp, e)),
                             (envArg, "to the following statments    ")])
Axel Simon's avatar
Axel Simon committed
611
         val env = E.reduceToResult env
Axel Simon's avatar
Axel Simon committed
612
613
614
      in
         env
      end
Axel Simon's avatar
Axel Simon committed
615

Axel Simon's avatar
Axel Simon committed
616
   and infDecodepat sym stenv (AST.MARKdecodepat m) =
Axel Simon's avatar
Axel Simon committed
617
      reportError (infDecodepat sym) stenv m
Axel Simon's avatar
Axel Simon committed
618
619
620
621
      | infDecodepat sym (st, env) (AST.TOKENdecodepat t) =
         let
            val envGra = E.pushWidth (granularitySymId, env)
            val envDec = E.pushWidth (sym, env)
Axel Simon's avatar
Axel Simon committed
622
            val env = E.meet (envGra, envDec)
Axel Simon's avatar
Axel Simon committed
623
624
625
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking decoder",
626
627
                            [(envGra, "granularity                     "),
                             (envDec, "token " ^ showProg (20, PP.tokpat, t))])
Axel Simon's avatar
Axel Simon committed
628
629
630
631
632
633
            val env = E.popKappa env
         in
            infTokpat (st, env) t
         end
     | infDecodepat sym (st,env) (AST.BITdecodepat l) =
      let
Axel Simon's avatar
Axel Simon committed
634
         val envGra = E.pushWidth (sym, env)
Julian Kranz's avatar
Julian Kranz committed
635
         (*val _ = TextIO.print ("**** decpat pushing granularity:\n" ^ E.topToString envGra)*)
Axel Simon's avatar
Axel Simon committed
636
637
         val envPat = List.foldl (fn (b,env) => infBitpatSize (st,env) b)
                                 env l
Axel Simon's avatar
fix    
Axel Simon committed
638
         (*val _ = TextIO.print ("**** decpat pushing " ^ Int.toString(List.length l) ^ " sizes:\n" ^ E.topToString envPat)*)
Axel Simon's avatar
Axel Simon committed
639
         val envPat = E.reduceToSum (List.length l,envPat)
Julian Kranz's avatar
Julian Kranz committed
640
         (*val _ = TextIO.print ("**** decpat sum:\n" ^ E.topToString envPat)*)
Axel Simon's avatar
Axel Simon committed
641
         val env = E.meet (envGra, envPat)
Axel Simon's avatar
Axel Simon committed
642
643
644
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking bits in token",
645
646
                            [(envGra, "granularity                     "),
                             (envPat, "pattern " ^ showProg (20, PP.decodepat, (AST.BITdecodepat l)))])
Axel Simon's avatar
Axel Simon committed
647
648
649
650
651
652
653
654
         val env = E.popKappa env
      in
         List.foldl (fn (b,(n,env)) => case infBitpat (st,env) b of
                        (nArgs, env) => (n+nArgs, env)) (0, env) l
      end
   and infBitpatSize stenv (AST.MARKbitpat m) =
         reportError infBitpatSize stenv m
     | infBitpatSize (st,env) (AST.BITSTRbitpat str) =
Axel Simon's avatar
Axel Simon committed
655
         E.pushType (false, CONST (getBitpatLitLength str), env)
Axel Simon's avatar
Axel Simon committed
656
     | infBitpatSize (st,env) (AST.NAMEDbitpat v) = E.pushWidth (v,env)
657
     | infBitpatSize (st,env) (AST.BITVECbitpat (v,s)) =
658
         E.pushType (false, CONST (getBitpatLitLength s), env)
Axel Simon's avatar
Axel Simon committed
659
660
661
   and infBitpat stenv (AST.MARKbitpat m) = reportError infBitpat stenv m
     | infBitpat (st,env) (AST.BITSTRbitpat str) = (0,env)
     | infBitpat (st,env) (AST.NAMEDbitpat v) =
662
         (1, E.pushSymbol (v, getSpan st, env))
663
     | infBitpat (st,env) (AST.BITVECbitpat (v,s)) =
Axel Simon's avatar
Axel Simon committed
664
665
666
      let
         val env = E.pushLambdaVar (v,env)
         val envVar = E.pushSymbol (v, getSpan st, env)
667
         val envWidth = E.pushType (false, VEC (CONST (getBitpatLitLength s)), env)
Axel Simon's avatar
Axel Simon committed
668
669
670
671
672
         val env = E.meet (envVar, envWidth)
         val env = E.popKappa env
      in
         (1, env)
      end
Axel Simon's avatar
Axel Simon committed
673
674
   and infTokpat stenv (AST.MARKtokpat m) = reportError infTokpat stenv m
     | infTokpat (st,env) (AST.TOKtokpat i) = (0, env)
675
     | infTokpat (st,env) (AST.NAMEDtokpat v) = (1, E.pushLambdaVar (v,env))
676
   and infMatch (st,env) (p,e) =
677
678
679
680
      let
         val (n,env) = infPat (st,env) p
         (*val _ = TextIO.print ("**** after pat:\n" ^ E.toString env)*)
         val envScru = E.popKappa env
681
         val envScru = E.pushSymbol (caseExpSymId, SymbolTable.noSpan, envScru)
682
         (*val _ = TextIO.print ("**** after case dup:\n" ^ E.toString envScru)*)
Axel Simon's avatar
Axel Simon committed
683
         val env = E.meetFlow (env, envScru)
Axel Simon's avatar
Axel Simon committed
684
685
686
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking case scrutinee",
687
688
                            [(envScru, "scrutinee and patterns so far "),
                             (env,     "pattern " ^ showProg (22, PP.pat, p))])
689
690
691
692
693
694
695
         (*val _ = TextIO.print ("**** after mgu:\n" ^ E.toString env)*)
         val env = E.popKappa env
         val env = infExp (st,env) e
         (*val _ = TextIO.print ("**** after expr:\n" ^ E.toString env)*)
      in
         E.return (n,env)
      end
696

697
698
699
700
701
702
703
704
705
706
707
708
   and infPat stenv (AST.MARKpat m) = reportError infPat stenv m
     | infPat (st,env) (AST.LITpat lit) = (0, infLit (st,env) lit)
     | infPat (st,env) (AST.IDpat v) =
      let
         val (t, env) = E.pushLambdaVar' (v,env)
      in
         (1, E.pushType (false, t, env))
      end
     | infPat (st,env) (AST.CONpat (c, SOME p)) =
      let
         val (n,envPat) = infPat (st,env) p
         val envPat = E.pushTop envPat
709
         val envPat = E.reduceToFunction (envPat,1)
Axel Simon's avatar
Axel Simon committed
710
711
         val envCon = E.popKappa envPat
         val envCon = infExp (st,envCon) (AST.CONexp c)
Axel Simon's avatar
Axel Simon committed
712
         val env = E.meetFlow (envCon,envPat)
713
714
715
716
717
718
719
720
721
722
         val env = E.reduceToResult env
      in
         (n, env)
      end
     | infPat (st,env) (AST.CONpat (c, NONE)) =
         (0, infExp (st,env) (AST.CONexp c))
     | infPat (st,env) (AST.WILDpat) = (0, E.pushTop env)
   and infLit (st,env) (AST.INTlit i) = E.pushType (false, ZENO, env)
     | infLit (st,env) (AST.FLTlit f) = E.pushType (false, FLOAT, env)
     | infLit (st,env) (AST.STRlit str) = E.pushType (false, UNIT, env)
Axel Simon's avatar
Axel Simon committed
723
     | infLit (st,env) (AST.VEClit str) =
Axel Simon's avatar
Axel Simon committed
724
         E.pushType (false, VEC (CONST (String.size str)), env)
Axel Simon's avatar
Axel Simon committed
725

Axel Simon's avatar
Axel Simon committed
726
   (*enforce the size constraints of the primitives*)
Axel Simon's avatar
Axel Simon committed
727
728
   val primEnv = E.primitiveEnvironment (Primitives.getSymbolTypes (),
                  SizeConstraint.fromList Primitives.primitiveSizeConstraints)
Axel Simon's avatar
Axel Simon committed
729

730
   val toplevelEnv = E.pushGroup
Axel Simon's avatar
Axel Simon committed
731
      (List.concat
732
         (List.map topDecl (ast : SpecAbstractTree.specification))
733
      , primEnv)
Axel Simon's avatar
Axel Simon committed
734
   (*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
735
736
737
738
739
   val toplevelEnv = List.foldl (fn (d,env) =>
                        infDecl ({span = SymbolTable.noSpan},env) d
                        handle TypeError => env
                     ) toplevelEnv (ast : SpecAbstractTree.specification)
   val toplevelEnv = calcFixpoint toplevelEnv
Axel Simon's avatar
Axel Simon committed
740
                        handle TypeError => toplevelEnv
741
   (*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759

   (* check if all exported functions can be run with an empty state *)
   fun checkDecoder s sym = case E.forceNoInputs (sym,toplevelEnv) of
        [] => ()
      | fs =>
         let
            val decStr = SymbolTable.getString(!SymbolTables.varTable, sym)
            fun genFieldStr (f,(sep,str)) = (", ", str ^ sep ^
                  SymbolTable.getString(!SymbolTables.fieldTable, f))
            val (_,fsStr) = List.foldl genFieldStr ("", "") fs
         in
            Error.errorAt (errStrm, s,
               [decStr," cannot be exported due to lacking fields: ", fsStr]
            )
         end
   fun checkExports _ (AST.MARKdecl {span=s, tree=t}) = checkExports s t
     | checkExports s (AST.EXPORTdecl vs) = List.app (checkDecoder s) vs
     | checkExports s _ = ()
760
   val _ = List.app (checkExports SymbolTable.noSpan) ast
761

Axel Simon's avatar
Axel Simon committed
762
   val (badSizes, primEnv) = E.popGroup (toplevelEnv, false)
Axel Simon's avatar
Axel Simon committed
763
   val _ = reportBadSizes badSizes
Axel Simon's avatar
Axel Simon committed
764
   val (badSizes, _) = E.popGroup (primEnv, false)
Axel Simon's avatar
Axel Simon committed
765
   val _ = reportBadSizes badSizes
Axel Simon's avatar
Axel Simon committed
766
   in
Axel Simon's avatar
Axel Simon committed
767
      !sm
Axel Simon's avatar
Axel Simon committed
768
769
770
771
772
773
774
   end

   val typeInferencePass =
      BasicControl.mkTracePassSimple
         {passName="typeInferencePass",
          pass=typeInferencePass}

775
   fun run (ti,spec) = let
Axel Simon's avatar
Axel Simon committed
776
777
778
      open CompilationMonad
   in
      getErrorStream >>= (fn errs =>
Axel Simon's avatar
Axel Simon committed
779
780
781
782
      return (typeInferencePass (errs, ti, spec)
         handle TypeError => []
         )
      )
Axel Simon's avatar
Axel Simon committed
783
   end
784
785
786
787
788
789
   
   val showTable = (fn (str,_) => str) o List.foldl (fn ((sym,st), (str,si)) =>
         let
            val sStr = SymbolTable.getString(!SymbolTables.varTable, sym)
         in
            case st of
Axel Simon's avatar
Axel Simon committed
790
                 E.VALUE {symType = t, symFlow = bFun} =>
791
792
793
                  let
                     val (tStr, si) = showTypeSI (t,si)
                  in
Axel Simon's avatar
Axel Simon committed
794
                     (sStr ^ " : " ^ tStr ^ ";" ^ BD.showBFun bFun ^ "\n" ^ str, si)
795
                  end
Axel Simon's avatar
Axel Simon committed
796
               | E.DECODE {symType = t, symFlow = bFun, width = w} =>
797
798
799
800
                  let
                     val (tStr, si) = showTypeSI (t,si)
                     val (wStr, si) = showTypeSI (w,si)
                  in
Axel Simon's avatar
Axel Simon committed
801
                     (sStr ^ " : " ^ tStr ^ ";" ^ BD.showBFun bFun ^ ", width = " ^
802
803
804
805
806
                      wStr ^ "\n" ^ str, si)
                  end
         end
      ) ("",TVar.emptyShowInfo)

Axel Simon's avatar
Axel Simon committed
807
end