inference.sml 32.9 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*)
134
   val maxIter = 2
Axel Simon's avatar
Axel Simon committed
135
   fun checkUsages printWarn (sym, env) =
Axel Simon's avatar
Axel Simon committed
136
      let
137
         (*val _ = TextIO.print ("***** usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
138
         fun checkUsage (s, (unstable, env)) =
Axel Simon's avatar
Axel Simon committed
139
            let
Axel Simon's avatar
Axel Simon committed
140
               val fs = E.getContextOfUsage (sym, s, env)
141
               val oldCtxt = E.getCtxt env
Axel Simon's avatar
Axel Simon committed
142
143
               val env = List.foldl E.pushFunction env fs
               
144
               val envFun = E.pushSymbol (sym, s, env)
145
               (*val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)*)
Axel Simon's avatar
Axel Simon committed
146
               val envCall = E.pushUsage (sym, s, !sm, env)
147
               (*val _ = TextIO.print ("pushed usage:\n" ^ E.topToString envCall)*)
Axel Simon's avatar
Axel Simon committed
148
149
150
               (*inform about a unification failure when checking call site
               with definition*)
               fun raiseError str =
Axel Simon's avatar
Axel Simon committed
151
                  let
Axel Simon's avatar
Axel Simon committed
152
                     val si = TVar.emptyShowInfo
Axel Simon's avatar
Axel Simon committed
153
154
155
156
157
158
                     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),
Axel Simon's avatar
Axel Simon committed
159
                     "\n\tcall provides type  " ^ sCall,
160
                     "\n\tdefinition has type " ^ sFun]))
Axel Simon's avatar
Axel Simon committed
161
                  end
Axel Simon's avatar
Axel Simon committed
162
163
               (*warn about refinement of definition due to a call site*)
               fun raiseWarning (substs, syms) =
Axel Simon's avatar
Axel Simon committed
164
165
                  if E.SymbolSet.isEmpty syms orelse not printWarn then ()
                  else
Axel Simon's avatar
Axel Simon committed
166
167
168
169
                  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
170
                        let
Axel Simon's avatar
Axel Simon committed
171
172
                           val sStr = SymbolTable.getString
                              (!SymbolTables.varTable, sym)
173
                           val (sType, si) = E.funTypeToStringSI (env, sym, si)
Axel Simon's avatar
Axel Simon committed
174
                        in
Axel Simon's avatar
Axel Simon committed
175
                           (res ^ pre ^ sStr ^ " : " ^ sType, ", ", si)
Axel Simon's avatar
Axel Simon committed
176
                        end
Axel Simon's avatar
Axel Simon committed
177
                     val (symsStr, _, _) =
178
179
                        List.foldl showSyms ("", "", si)
                           (E.SymbolSet.listItems syms)
Axel Simon's avatar
Axel Simon committed
180
181
182
183
184
                  in 
                     (Error.warningAt (errStrm, s, [
                     "call to ",
                     SymbolTable.getString(!SymbolTables.varTable, sym),
                     " requires refinement ", sSubst,
185
                     "\n\tfor " ^ symsStr]))
Axel Simon's avatar
Axel Simon committed
186
                  end
Axel Simon's avatar
Axel Simon committed
187
               val (substs, env) = (E.subseteq (envCall, envFun),
Axel Simon's avatar
Axel Simon committed
188
                                         E.meetFlow (envCall, envFun))
Axel Simon's avatar
Axel Simon committed
189
                  handle (S.UnificationFailure str) =>
Axel Simon's avatar
Axel Simon committed
190
                     (raiseError str; (S.emptySubsts, envCall))
191
               val (changed, env) = E.popToUsage (sym, s, oldCtxt, env)
192
193
194
195
196
               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
197
               val affectedSyms = E.affectedFunctions (substs,envCall)
198
               val _ = raiseWarning (substs, affectedSyms)
Axel Simon's avatar
Axel Simon committed
199
            in
Axel Simon's avatar
Axel Simon committed
200
               (E.SymbolSet.union (unstable, affectedSyms), env)
Axel Simon's avatar
Axel Simon committed
201
            end
Axel Simon's avatar
Axel Simon committed
202
      in
Axel Simon's avatar
Axel Simon committed
203
204
205
         List.foldl checkUsage (E.SymbolSet.empty, env) (E.getUsages (sym, env))
      end

Axel Simon's avatar
Axel Simon committed
206
   fun checkCallSites printWarn (syms, env) =
Axel Simon's avatar
Axel Simon committed
207
      List.foldl (fn (sym, (unstable, env)) =>
Axel Simon's avatar
Axel Simon committed
208
                  case checkUsages printWarn (sym, env) of
Axel Simon's avatar
Axel Simon committed
209
210
211
212
                     (newUnstable, env) =>
                        (E.SymbolSet.union (unstable,newUnstable), env)
                  ) (E.SymbolSet.empty, env) (E.SymbolSet.listItems syms)

213
   fun calcFixpoint curIter (syms, env) =
Axel Simon's avatar
Axel Simon committed
214
         if E.SymbolSet.isEmpty syms then env else
215
         if curIter<maxIter then
Axel Simon's avatar
Axel Simon committed
216
217
            calcFixpoint (curIter+1)
               (checkCallSites (curIter=maxIter) (syms, env))
Axel Simon's avatar
Axel Simon committed
218
         else
Axel Simon's avatar
Axel Simon committed
219
220
221
222
223
224
         let
            val si = TVar.emptyShowInfo
            fun showSyms (sym, (res, pre, si)) =
               let
                  val sStr = SymbolTable.getString
                     (!SymbolTables.varTable, sym)
225
                  val env = E.pushSymbol (sym, SymbolTable.noSpan, env)
Axel Simon's avatar
Axel Simon committed
226
227
228
229
230
231
232
233
234
235
236
237
                  val (sType, si) = E.kappaToStringSI (env, si)
               in
                  (res ^ pre ^ sStr ^ " : " ^ sType, ", ", si)
               end
            val symIds = E.SymbolSet.listItems syms
            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,
238
            "\n\tpass --inference-iterations=",
Axel Simon's avatar
Axel Simon committed
239
240
241
242
243
            Int.toString (maxIter+1),
            " to try a little harder"]); env)
         end
   val calcFixpoint = calcFixpoint 0
   
244
   fun infRhs (st,env) (sym, dec, guard, args, rhs) =
Axel Simon's avatar
Axel Simon committed
245
      let
246
         (*val _ = TextIO.print ("checking binding " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
247
248
         fun checkGuard (g,env) =
            let
249
250
251
               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
252
               val envGua = infExp (st, env) g
Axel Simon's avatar
Axel Simon committed
253
               val env = E.meet (envRef, envGua)
254
255
256
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking guards",
257
258
                            [(envRef, "required guard type        "),
                             (envGua, "guard " ^ showProg (20, PP.exp, g))])
Axel Simon's avatar
Axel Simon committed
259
260
261
262
263
            in
               E.popKappa env
            end
         val env = case guard of SOME g => checkGuard (g,env)
                               | NONE => env
Axel Simon's avatar
Axel Simon committed
264
265
266
         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
267
         val env = List.foldl E.pushLambdaVar env args
268
         val rhs = decsToSeq rhs dec
Axel Simon's avatar
Axel Simon committed
269
         val env = infExp (st,env) rhs
270
         val env = E.reduceToFunction (env, List.length args)
Axel Simon's avatar
Axel Simon committed
271
         val env = E.return (n,env)
272
         (*val _ = TextIO.print ("after popping args:\n" ^ E.topToString env)*)
Axel Simon's avatar
Axel Simon committed
273
      in
274
         env
Axel Simon's avatar
Axel Simon committed
275
      end
Axel Simon's avatar
Axel Simon committed
276
   and infBinding (st,env) (sym, args, rhs) =
Axel Simon's avatar
Axel Simon committed
277
      let
278
         val env = E.pushFunction (sym,env)
279
         val env = infRhs (st,env) (sym, [], NONE, args, rhs)
Axel Simon's avatar
Axel Simon committed
280
281
282
         val env = E.popToFunction (sym, env)
         val fInfo = E.getFunctionInfo (sym, env)
         val _ = sm := (sym, fInfo) :: !sm
283
         val (unstable, env) = checkUsages false (sym, env)
Axel Simon's avatar
Axel Simon committed
284
      in
285
         (unstable, env)
Axel Simon's avatar
Axel Simon committed
286
      end
287

Axel Simon's avatar
Axel Simon committed
288
   and infDecl stenv (AST.MARKdecl m) = reportError infDecl stenv m
Axel Simon's avatar
Axel Simon committed
289
290
291
     | infDecl (st,env) (AST.GRANULARITYdecl w) =
      let
         val envGra = E.pushWidth (granularitySymId, env)
Axel Simon's avatar
Axel Simon committed
292
         val envInt = E.pushType (false, CONST (IntInf.toInt w), env)
Axel Simon's avatar
Axel Simon committed
293
         val env = E.meet (envGra, envInt)
Axel Simon's avatar
Axel Simon committed
294
295
296
297
         val env = E.popKappa env
      in
         (E.SymbolSet.empty, env)
      end
Axel Simon's avatar
Axel Simon committed
298
     | infDecl stenv (AST.DECODEdecl dd) = infDecodedecl stenv dd
Axel Simon's avatar
Axel Simon committed
299
     | infDecl (st,env) (AST.LETRECdecl (v,l,e)) =
Axel Simon's avatar
Axel Simon committed
300
         infBinding (st,env) (v, l, e)
Axel Simon's avatar
Axel Simon committed
301
     | infDecl (st,env) _ = (E.SymbolSet.empty, env)
302

303
   and infDecodedecl (st,env) (v, l, Sum.INL e) =
Axel Simon's avatar
Axel Simon committed
304
305
306
      let
         val env = E.pushFunctionOrTop (v,env)
         val envRhs = E.popKappa env
307
         val envRhs = infRhs (st,envRhs) (v, l, NONE, [], e)
308
309
         (*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
310
         val env = E.meet (env, envRhs)
Axel Simon's avatar
Axel Simon committed
311
         val env = E.popToFunction (v, env)
Axel Simon's avatar
Axel Simon committed
312
         val fInfo = E.getFunctionInfo (v, env)
Axel Simon's avatar
Axel Simon committed
313
314
         val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
                                       not (SymbolTable.eq_symid(s,v))) (!sm)
Axel Simon's avatar
Axel Simon committed
315
      in
Axel Simon's avatar
Axel Simon committed
316
         (E.SymbolSet.singleton v, env)
Axel Simon's avatar
Axel Simon committed
317
      end
318
     | infDecodedecl (st,env) (v, l, Sum.INR el) =
319
      let
Axel Simon's avatar
Axel Simon committed
320
         val env = E.pushFunctionOrTop (v,env)
321
322
323
         val env = List.foldl
            (fn ((guard, rhs), env) => let
               val envRhs = E.popKappa env
324
               val envRhs = infRhs (st,envRhs) (v, l, SOME guard, [], rhs)
Axel Simon's avatar
Axel Simon committed
325
               val env = E.meet (env, envRhs)
326
327
328
            in
               env
            end) env el
Axel Simon's avatar
Axel Simon committed
329
         val env = E.popToFunction (v, env)
Axel Simon's avatar
Axel Simon committed
330
         val fInfo = E.getFunctionInfo (v, env)
Axel Simon's avatar
Axel Simon committed
331
332
         val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
                                       not (SymbolTable.eq_symid(s,v))) (!sm)
333
      in
Axel Simon's avatar
Axel Simon committed
334
         (E.SymbolSet.singleton v, env)
335
      end
336

337
   and infExp stenv (AST.MARKexp m) = reportError infExp stenv m
338
     | infExp (st,env) (AST.LETRECexp (l,e)) =
Axel Simon's avatar
Axel Simon committed
339
      let                                              
340
         val names = List.map topLetrecDecl l
Axel Simon's avatar
Axel Simon committed
341
342
         val env = E.pushGroup (List.concat names, env)
         val (unstable, env) = List.foldl (fn ((v,l,e), (unstable, env)) =>
Axel Simon's avatar
Axel Simon committed
343
               case infBinding (st, env) (v, l, e) of
Axel Simon's avatar
Axel Simon committed
344
345
346
347
348
                  (newUnstable, env) =>
                     (E.SymbolSet.union (newUnstable, unstable), env)
            ) (E.SymbolSet.empty, env) l
         val env = calcFixpoint (unstable, env)
         val env = infExp (st,env) e
Axel Simon's avatar
Axel Simon committed
349
         val (badSizes, env) = E.popGroup (env, true)
Axel Simon's avatar
Axel Simon committed
350
         val _ = reportBadSizes badSizes
Axel Simon's avatar
Axel Simon committed
351
      in
Axel Simon's avatar
Axel Simon committed
352
         env
Axel Simon's avatar
Axel Simon committed
353
354
355
      end
     | infExp (st,env) (AST.IFexp (e1,e2,e3)) =
      let
356
357
         val envWant = E.pushType (false, VEC (CONST 1), env)
         val envHave = infExp (st,env) e1
Axel Simon's avatar
Axel Simon committed
358
         val env = E.meet (envWant, envHave)
359
         val env = E.popKappa env
Axel Simon's avatar
Axel Simon committed
360
         val envT = infExp (st,env) e2
361
         (*val _ = TextIO.print ("**** after if-then:\n" ^ E.topToString envT)*)
Axel Simon's avatar
Axel Simon committed
362
         val envE = infExp (st,env) e3
363
         (*val _ = TextIO.print ("**** after if-else:\n" ^ E.topToString envE)*)
364
         val env = E.meet (envE,envT)
Axel Simon's avatar
Axel Simon committed
365
366
367
      in
         env
      end
368
369
370
371
     | infExp (st,env) (AST.CASEexp (e,l)) =
      let
         val (t,env) = E.pushLambdaVar' (caseExpSymId, env)
         val envExp = infExp (st,env) e
372
         (*val _ = TextIO.print ("**** after case exp:\n" ^ E.toString envExp)*)
373
         val envVar = E.pushType (false, t, env)
374
         (*val _ = TextIO.print ("**** after case dup:\n" ^ E.toString envVar)*)
Axel Simon's avatar
Axel Simon committed
375
         val env = E.meetFlow (envVar, envExp)
376
377
         val env = E.popKappa env
         val envNeutral = E.pushTop env
Axel Simon's avatar
Axel Simon committed
378
         fun genFlow ((p,exp), nEnv) =
379
            let
Axel Simon's avatar
Axel Simon committed
380
               val expEnv = infMatch (st,E.popKappa nEnv) (p,exp)
Axel Simon's avatar
Axel Simon committed
381
               val env = E.meetFlow (nEnv, expEnv)
Axel Simon's avatar
Axel Simon committed
382
                  handle S.UnificationFailure str =>
Axel Simon's avatar
Axel Simon committed
383
384
                     refineError (str,
                                  " while checking right-hand-side of branches",
385
386
                                  [(nEnv, "branches so far               "),
                                   (expEnv, showProg (30, PP.exp, exp))])
387
            in
Axel Simon's avatar
Axel Simon committed
388
               env
389
            end
Axel Simon's avatar
Axel Simon committed
390
         val env = List.foldl genFlow envNeutral l
391
392
393
394
         (*val _ = TextIO.print ("**** all envs:\n" ^ E.toString env)*)
      in
         E.return (1,env)
      end
395
396
397
398
399
400
     | 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
401
         infExp stenv (AST.APPLYexp (infixToExp binop, [e1, e2]))
402
      end
403
     | infExp (st,env) (AST.APPLYexp (e1,es2)) =
Axel Simon's avatar
Axel Simon committed
404
      let                                      
405
         val envFun = infExp (st,env) e1
406
         val envArg = List.foldl (fn (e2,env) => infExp (st,env) e2) env es2
407
408
         (*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
409
         val envArgRes = E.pushTop envArg
410
         val envArgRes = E.reduceToFunction (envArgRes, List.length es2)
411
         (*val _ = TextIO.print ("**** app turning arg:\n" ^ E.toString envArgRes)*)
Axel Simon's avatar
Axel Simon committed
412
413
414
415
         (* 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
416
            handle S.UnificationFailure str =>
Axel Simon's avatar
Axel Simon committed
417
418
               refineError (str,
                            " while passing",
419
420
421
422
423
                            (#1 (List.foldr
                            (fn (e2,(res,env)) => 
                              ((env, "argument    " ^ showProg (20, PP.exp, e2))::res,
                               E.popKappa env)
                            ) ([], envArg) es2)) @
424
                            [(envFun, "to function " ^ showProg (20, PP.exp, e1))])
Axel Simon's avatar
Axel Simon committed
425
         (*val _ = TextIO.print ("**** app fun,res unified:\n" ^ E.topToString env)*)
Axel Simon's avatar
Axel Simon committed
426
         val env = E.reduceToResult env
427
      in
Axel Simon's avatar
Axel Simon committed
428
         env                                                         
429
430
      end
        
431
432
     | infExp (st,env) (AST.RECORDexp l) =
      let
433
434
         val t = freshVar ()
         val env = E.meetBoolean (BD.meetVarZero (bvar t), env)
435
         val env = E.pushType (false, t, env)
436
437
         fun pushField ((fid,e), (nts, env)) =
            let
438
               val env = infExp (st,env) e
439
               val bVar = BD.freshBVar ()
440
               val env = E.meetBoolean (BD.meetVarOne bVar, env)
441
            in
442
               ((bVar, fid) :: nts, env)
443
444
            end
         val (nts, env) = List.foldl pushField ([], env) l
445
         (*val _ = TextIO.print ("**** rec exp, single fields:\n" ^ E.toString env ^ "\n")*)
446
         val env = E.reduceToRecord (nts, env)
447
         (*val _ = TextIO.print ("**** rec exp, combined:\n" ^ E.toString env ^ "\n")*)
448
449
450
451
452
453
454
      in
         env
      end
         
     | infExp (st,env) (AST.SELECTexp f) =
      let
         val env = E.pushTop env
455
456
         val tf = freshVar ()
         val tf' = newFlow tf
457
458
         val env = E.pushType (false, tf, env)
         val exists = BD.freshBVar ()
Axel Simon's avatar
Axel Simon committed
459
         (*val _ = TextIO.print ("**** before rec reduce:\n" ^ E.toString env ^ "\n")*)
460
         val env = E.reduceToRecord ([(exists, f)], env)
Axel Simon's avatar
Axel Simon committed
461
         val env = E.meetBoolean (BD.meetVarImpliesVar (bvar tf', bvar tf) o
462
                                  BD.meetVarOne exists, env)
Axel Simon's avatar
Axel Simon committed
463
         (*val _ = TextIO.print ("**** after rec reduce:\n" ^ E.toString env ^ "\n")*)
464
         val env = E.pushType (false, tf', env)
465
         val env = E.reduceToFunction (env,1)
466
         (*val _ = TextIO.print ("**** rec selector:\n" ^ E.topToString env ^ "\n")*)
467
468
469
      in
         env
      end
470
     | infExp (st,env) (AST.UPDATEexp fs) =
471
      let
472
         val fieldsVar = freshVar ()
473
474
475
476
477
478
479
480
481
482
483
         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)

484
485
486
         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
487
         fun pushOutField ((fid,eOpt), (nts, env)) =
488
            let
489
               (*val _ = TextIO.print ("**** rec update: pushing field " ^ SymbolTable.getString(!SymbolTables.fieldTable, fid) ^ ".\n")*)
490
               val bVar = BD.freshBVar ()
Axel Simon's avatar
Axel Simon committed
491
492
493
494
495
               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)
496
            in
497
               ((bVar, fid) :: nts, env)
498
499
500
            end
         val (nts, env) = List.foldl pushOutField ([], env) fs
         val env = E.reduceToRecord (nts, env)
501
         val env = E.reduceToFunction (env,1)
502
         (*val _ = TextIO.print ("**** rec update: function is:\n" ^ E.topToString env ^ "\n")*)
503
504
505
      in
         env
      end
Axel Simon's avatar
Axel Simon committed
506
507
     | infExp stenv (AST.LITexp lit) = infLit stenv lit
     | infExp stenv (AST.SEQexp l) = infSeqexp stenv l
Axel Simon's avatar
Axel Simon committed
508
509
     | infExp (st,env) (AST.IDexp v) =
      let
510
         val env = E.pushSymbol (v, getSpan st, env)
511
         (*val _ = TextIO.print ("**** after pushing symbol " ^ SymbolTable.getString(!SymbolTables.varTable, v) ^ ":\n" ^ E.topToString env)*)
Axel Simon's avatar
Axel Simon committed
512
513
514
      in
         env
      end
515
516
517
518
519
     | 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)
520
521
522
523
         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
524
525
526
527
528
            let
               val (posFlags, negFlags) =
                  fieldBVarsets (t,(BD.emptySet, BD.emptySet))
               val env = E.meetBoolean (BD.meetVarSetOne posFlags o
                                        BD.meetVarSetZero negFlags, env)
529
               val env = E.pushType (true, FUN ([t],ALG (dcon, List.map VAR vs)), env)
Axel Simon's avatar
Axel Simon committed
530
531
532
            in
               env
            end
533
         (*val _ = TextIO.print ("**** looking for " ^ SymbolTable.getString(!SymbolTables.conTable, c) ^ ":\n" ^ E.topToString env)*)
534
      in
535
         env
536
      end
537
538
539
540
541
542
543
     | 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
544
         
Axel Simon's avatar
Axel Simon committed
545
546
547
548
   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
549
550
     | infSeqexp (st,env) [AST.ACTIONseqexp e] = infExp (st,env) e
     | infSeqexp (st,env) (s :: l) =
Axel Simon's avatar
Axel Simon committed
551
      let
Axel Simon's avatar
Axel Simon committed
552
553
554
555
         val (bind, vOpt,e) = case s of
               AST.ACTIONseqexp e => (bindSymId, NONE, e)
             | AST.BINDseqexp (v,e) => (bindASymId, SOME v, e)
             | _ => raise TypeError
556
         val envFun = E.pushSymbol (bind, getSpan st, env)
Axel Simon's avatar
Axel Simon committed
557
558
         val envArg = infExp (st,env) e
         val envArgRes = E.pushTop envArg
559
         val envArgRes = E.reduceToFunction (envArgRes,1)
560
         (*val _ = TextIO.print ("function to unify with bind: " ^ E.topToString envArgRes ^ "\n")*)
Axel Simon's avatar
Axel Simon committed
561
         val env = E.meetFlow (envArgRes, envFun)
Axel Simon's avatar
Axel Simon committed
562
            handle S.UnificationFailure str =>
Axel Simon's avatar
Axel Simon committed
563
564
565
566
567
568
               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
569
                 SOME v => E.reduceToFunction (infSeqexp (st, E.pushLambdaVar (v,env)) l,1)
Axel Simon's avatar
Axel Simon committed
570
571
               | NONE => infSeqexp (st, env) l
         val envArgRes = E.pushTop envArg
572
         val envArgRes = E.reduceToFunction (envArgRes,1)
Axel Simon's avatar
Axel Simon committed
573
         val env = E.meetFlow (envArgRes, envFun)
Axel Simon's avatar
Axel Simon committed
574
575
            handle S.UnificationFailure str =>
               refineError (str,
Axel Simon's avatar
Axel Simon committed
576
                            " when passing on the result of",
577
578
                            [(envFun, "statement " ^ showProg (20, PP.exp, e)),
                             (envArg, "to the following statments    ")])
Axel Simon's avatar
Axel Simon committed
579
         val env = E.reduceToResult env
Axel Simon's avatar
Axel Simon committed
580
581
582
      in
         env
      end
Axel Simon's avatar
Axel Simon committed
583

Axel Simon's avatar
Axel Simon committed
584
   and infDecodepat sym stenv (AST.MARKdecodepat m) =
Axel Simon's avatar
Axel Simon committed
585
      reportError (infDecodepat sym) stenv m
Axel Simon's avatar
Axel Simon committed
586
587
588
589
      | 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
590
            val env = E.meet (envGra, envDec)
Axel Simon's avatar
Axel Simon committed
591
592
593
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking decoder",
594
595
                            [(envGra, "granularity                     "),
                             (envDec, "token " ^ showProg (20, PP.tokpat, t))])
Axel Simon's avatar
Axel Simon committed
596
597
598
599
600
601
            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
602
         val envGra = E.pushWidth (sym, env)
Julian Kranz's avatar
Julian Kranz committed
603
         (*val _ = TextIO.print ("**** decpat pushing granularity:\n" ^ E.topToString envGra)*)
Axel Simon's avatar
Axel Simon committed
604
605
         val envPat = List.foldl (fn (b,env) => infBitpatSize (st,env) b)
                                 env l
Axel Simon's avatar
fix    
Axel Simon committed
606
         (*val _ = TextIO.print ("**** decpat pushing " ^ Int.toString(List.length l) ^ " sizes:\n" ^ E.topToString envPat)*)
Axel Simon's avatar
Axel Simon committed
607
         val envPat = E.reduceToSum (List.length l,envPat)
Julian Kranz's avatar
Julian Kranz committed
608
         (*val _ = TextIO.print ("**** decpat sum:\n" ^ E.topToString envPat)*)
Axel Simon's avatar
Axel Simon committed
609
         val env = E.meet (envGra, envPat)
Axel Simon's avatar
Axel Simon committed
610
611
612
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking bits in token",
613
614
                            [(envGra, "granularity                     "),
                             (envPat, "pattern " ^ showProg (20, PP.decodepat, (AST.BITdecodepat l)))])
Axel Simon's avatar
Axel Simon committed
615
616
617
618
619
620
621
622
         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
623
         E.pushType (false, CONST (getBitpatLitLength str), env)
Axel Simon's avatar
Axel Simon committed
624
     | infBitpatSize (st,env) (AST.NAMEDbitpat v) = E.pushWidth (v,env)
625
     | infBitpatSize (st,env) (AST.BITVECbitpat (v,s)) =
626
         E.pushType (false, CONST (getBitpatLitLength s), env)
Axel Simon's avatar
Axel Simon committed
627
628
629
   and infBitpat stenv (AST.MARKbitpat m) = reportError infBitpat stenv m
     | infBitpat (st,env) (AST.BITSTRbitpat str) = (0,env)
     | infBitpat (st,env) (AST.NAMEDbitpat v) =
630
         (1, E.pushSymbol (v, getSpan st, env))
631
     | infBitpat (st,env) (AST.BITVECbitpat (v,s)) =
Axel Simon's avatar
Axel Simon committed
632
633
634
      let
         val env = E.pushLambdaVar (v,env)
         val envVar = E.pushSymbol (v, getSpan st, env)
635
         val envWidth = E.pushType (false, VEC (CONST (getBitpatLitLength s)), env)
Axel Simon's avatar
Axel Simon committed
636
637
638
639
640
         val env = E.meet (envVar, envWidth)
         val env = E.popKappa env
      in
         (1, env)
      end
Axel Simon's avatar
Axel Simon committed
641
642
   and infTokpat stenv (AST.MARKtokpat m) = reportError infTokpat stenv m
     | infTokpat (st,env) (AST.TOKtokpat i) = (0, env)
643
     | infTokpat (st,env) (AST.NAMEDtokpat v) = (1, E.pushLambdaVar (v,env))
644
   and infMatch (st,env) (p,e) =
645
646
647
648
      let
         val (n,env) = infPat (st,env) p
         (*val _ = TextIO.print ("**** after pat:\n" ^ E.toString env)*)
         val envScru = E.popKappa env
649
         val envScru = E.pushSymbol (caseExpSymId, SymbolTable.noSpan, envScru)
650
         (*val _ = TextIO.print ("**** after case dup:\n" ^ E.toString envScru)*)
Axel Simon's avatar
Axel Simon committed
651
         val env = E.meetFlow (env, envScru)
Axel Simon's avatar
Axel Simon committed
652
653
654
            handle S.UnificationFailure str =>
               refineError (str,
                            " when checking case scrutinee",
655
656
                            [(envScru, "scrutinee and patterns so far "),
                             (env,     "pattern " ^ showProg (22, PP.pat, p))])
657
658
659
660
661
662
663
         (*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
664

665
666
667
668
669
670
671
672
673
674
675
676
   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
677
         val envPat = E.reduceToFunction (envPat,1)
Axel Simon's avatar
Axel Simon committed
678
679
         val envCon = E.popKappa envPat
         val envCon = infExp (st,envCon) (AST.CONexp c)
Axel Simon's avatar
Axel Simon committed
680
         val env = E.meetFlow (envCon,envPat)
681
682
683
684
685
686
687
688
689
690
         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
691
     | infLit (st,env) (AST.VEClit str) =
Axel Simon's avatar
Axel Simon committed
692
         E.pushType (false, VEC (CONST (String.size str)), env)
Axel Simon's avatar
Axel Simon committed
693

Axel Simon's avatar
Axel Simon committed
694
   (*enforce the size constraints of the primitives*)
Axel Simon's avatar
Axel Simon committed
695
696
   val primEnv = E.primitiveEnvironment (Primitives.getSymbolTypes (),
                  SizeConstraint.fromList Primitives.primitiveSizeConstraints)
Axel Simon's avatar
Axel Simon committed
697

698
   val toplevelEnv = E.pushGroup
Axel Simon's avatar
Axel Simon committed
699
      (List.concat
700
         (List.map topDecl (ast : SpecAbstractTree.specification))
701
      , primEnv)
Axel Simon's avatar
Axel Simon committed
702
   (*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
Axel Simon's avatar
Axel Simon committed
703
   val (unstable, toplevelEnv) = List.foldl (fn (d,(unstable, env)) =>
704
            (case infDecl ({span = SymbolTable.noSpan},env) d of
Axel Simon's avatar
Axel Simon committed
705
               (newUnstable, env) =>
Axel Simon's avatar
Axel Simon committed
706
707
                  (E.SymbolSet.union (newUnstable, unstable), env))
               handle TypeError => (unstable, env)
Axel Simon's avatar
Axel Simon committed
708
         ) (E.SymbolSet.empty, toplevelEnv)
709
         (ast : SpecAbstractTree.specification)
Axel Simon's avatar
Axel Simon committed
710
   val toplevelEnv = calcFixpoint (unstable, toplevelEnv)
Axel Simon's avatar
Axel Simon committed
711
                        handle TypeError => toplevelEnv
712
   (*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730

   (* 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 _ = ()
731
   val _ = List.app (checkExports SymbolTable.noSpan) ast
732

Axel Simon's avatar
Axel Simon committed
733
   val (badSizes, primEnv) = E.popGroup (toplevelEnv, false)
Axel Simon's avatar
Axel Simon committed
734
   val _ = reportBadSizes badSizes
Axel Simon's avatar
Axel Simon committed
735
   val (badSizes, _) = E.popGroup (primEnv, false)
Axel Simon's avatar
Axel Simon committed
736
   val _ = reportBadSizes badSizes
Axel Simon's avatar
Axel Simon committed
737
   in
Axel Simon's avatar
Axel Simon committed
738
      !sm
Axel Simon's avatar
Axel Simon committed
739
740
741
742
743
744
745
   end

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

746
   fun run (ti,spec) = let
Axel Simon's avatar
Axel Simon committed
747
748
749
      open CompilationMonad
   in
      getErrorStream >>= (fn errs =>
Axel Simon's avatar
Axel Simon committed
750
751
752
753
      return (typeInferencePass (errs, ti, spec)
         handle TypeError => []
         )
      )
Axel Simon's avatar
Axel Simon committed
754
   end
755
756
757
758
759
760
   
   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
761
                 E.VALUE {symType = t, symFlow = bFun} =>
762
763
764
                  let
                     val (tStr, si) = showTypeSI (t,si)
                  in
Axel Simon's avatar
Axel Simon committed
765
                     (sStr ^ " : " ^ tStr ^ ";" ^ BD.showBFun bFun ^ "\n" ^ str, si)
766
                  end
Axel Simon's avatar
Axel Simon committed
767
               | E.DECODE {symType = t, symFlow = bFun, width = w} =>
768
769
770
771
                  let
                     val (tStr, si) = showTypeSI (t,si)
                     val (wStr, si) = showTypeSI (w,si)
                  in
Axel Simon's avatar
Axel Simon committed
772
                     (sStr ^ " : " ^ tStr ^ ";" ^ BD.showBFun bFun ^ ", width = " ^
773
774
775
776
777
                      wStr ^ "\n" ^ str, si)
                  end
         end
      ) ("",TVar.emptyShowInfo)

Axel Simon's avatar
Axel Simon committed
778
end